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