doc-src/Logics/preface.tex
author paulson
Wed, 13 Jan 1999 16:30:53 +0100
changeset 6120 f40d61cd6b32
child 6148 d97a944c6ea3
permissions -rw-r--r--
removal of FOL and ZF
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6120
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
     1
%% $Id$
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
     2
\chapter*{Preface}
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
     3
Several logics come with Isabelle.  Many of them are sufficiently developed
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
     4
to serve as comfortable reasoning environments.  They are also good
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
     5
starting points for defining new logics.  Each logic is distributed with
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
     6
sample proofs, some of which are described in this document.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
     7
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
     8
The logics \texttt{FOL} (first-order logic) and \texttt{ZF} (axiomatic set
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
     9
theory) are described in a separate manual~\cite{isabelle-ZF}.  Here are the
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    10
others:
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    11
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    12
\begin{ttdescription}
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    13
\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    14
  which is the basis of a preliminary method for deriving programs from
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    15
  proofs~\cite{coen92}.  It is built upon classical~\FOL{}.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    16
 
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    17
\item[\thydx{LCF}] is a version of Scott's Logic for Computable
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    18
  Functions, which is also implemented by the~{\sc lcf}
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    19
  system~\cite{paulson87}.  It is built upon classical~\FOL{}.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    20
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    21
\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40},
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    22
which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    23
This object-logic should not be confused with Isabelle's meta-logic, which is
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    24
also a form of higher-order logic.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    25
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    26
\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    27
  extension of \texttt{HOL}\@.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    28
 
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    29
\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    30
Theory~\cite{nordstrom90}, with extensional equality.  Universes are not
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    31
included.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    32
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    33
\item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    34
 \end{ttdescription}
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    35
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    36
The directory \texttt{Sequents} contains several logics based
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    37
  upon the sequent calculus.  Sequents have the form $A@1,\ldots,A@m\turn
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    38
B@1,\ldots,B@n$; rules are applied using associative matching.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    39
\begin{ttdescription}
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    40
\item[\thydx{LK}] is classical first-order logic as a sequent calculus.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    41
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    42
\item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$.  
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    43
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    44
\item[\thydx{ILL}] implements intuitionistic linear logic.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    45
\end{ttdescription}
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    46
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    47
The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    48
  Cube} are undocumented.  All object-logics' sources are
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    49
distributed with Isabelle (see the directory \texttt{src}).  They are
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    50
also available for browsing on the WWW at
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    51
\begin{ttbox}
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    52
http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    53
\end{ttbox}
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    54
Note that this is not necessarily consistent with your local sources!
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    55
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    56
\medskip Do not read this manual before reading \emph{Introduction to
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    57
  Isabelle} and performing some Isabelle proofs.  Consult the {\em Reference
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    58
  Manual} for more information on tactics, packages, etc.
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    59
f40d61cd6b32 removal of FOL and ZF
paulson
parents:
diff changeset
    60