1 \chapter*{Preface} |
|
2 Several logics come with Isabelle. Many of them are sufficiently developed |
|
3 to serve as comfortable reasoning environments. They are also good |
|
4 starting points for defining new logics. Each logic is distributed with |
|
5 sample proofs, some of which are described in this document. |
|
6 |
|
7 \texttt{HOL} is currently the best developed Isabelle object-logic, including |
|
8 an extensive library of (concrete) mathematics, and various packages for |
|
9 advanced definitional concepts (like (co-)inductive sets and types, |
|
10 well-founded recursion etc.). The distribution also includes some large |
|
11 applications. See the separate manual \emph{Isabelle's Logics: HOL}. There |
|
12 is also a comprehensive tutorial on Isabelle/HOL available. |
|
13 |
|
14 \texttt{ZF} provides another starting point for applications, with a slightly |
|
15 less developed library than \texttt{HOL}. \texttt{ZF}'s definitional packages |
|
16 are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides |
|
17 more advanced constructions for sets than simply-typed \texttt{HOL}. |
|
18 \texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described |
|
19 in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}. |
|
20 |
|
21 \medskip There are some further logics distributed with Isabelle: |
|
22 \begin{ttdescription} |
|
23 \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic, |
|
24 which is the basis of a preliminary method for deriving programs from |
|
25 proofs~\cite{coen92}. It is built upon classical~FOL. |
|
26 |
|
27 \item[\thydx{LCF}] is a version of Scott's Logic for Computable |
|
28 Functions, which is also implemented by the~{\sc lcf} |
|
29 system~\cite{paulson87}. It is built upon classical~FOL. |
|
30 |
|
31 \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of |
|
32 \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}. |
|
33 |
|
34 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type |
|
35 Theory~\cite{nordstrom90}, with extensional equality. Universes are not |
|
36 included. |
|
37 |
|
38 \item[\thydx{Cube}] is Barendregt's $\lambda$-cube. |
|
39 \end{ttdescription} |
|
40 |
|
41 The directory \texttt{Sequents} contains several logics based |
|
42 upon the sequent calculus. Sequents have the form $A@1,\ldots,A@m\turn |
|
43 B@1,\ldots,B@n$; rules are applied using associative matching. |
|
44 \begin{ttdescription} |
|
45 \item[\thydx{LK}] is classical first-order logic as a sequent calculus. |
|
46 |
|
47 \item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$. |
|
48 |
|
49 \item[\thydx{ILL}] implements intuitionistic linear logic. |
|
50 \end{ttdescription} |
|
51 |
|
52 The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt |
|
53 Cube} are undocumented. All object-logics' sources are distributed with |
|
54 Isabelle (see the directory \texttt{src}). They are also available for |
|
55 browsing on the WWW at |
|
56 |
|
57 \begin{center}\small |
|
58 \begin{tabular}{l} |
|
59 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ |
|
60 \url{http://isabelle.in.tum.de/library/} \\ |
|
61 \end{tabular} |
|
62 \end{center} |
|
63 |
|
64 Note that this is not necessarily consistent with your local sources! |
|
65 |
|
66 \medskip Do not read the \emph{Isabelle's Logics} manuals before reading |
|
67 \emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and |
|
68 performing some Isabelle proofs. Consult the {\em Reference Manual} for more |
|
69 information on tactics, packages, etc. |
|
70 |
|
71 |
|
72 %%% Local Variables: |
|
73 %%% mode: latex |
|
74 %%% TeX-master: "logics" |
|
75 %%% End: |
|