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.
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
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{}.
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{}.
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.
26 \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an
27 extension of \texttt{HOL}\@.
29 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
30 Theory~\cite{nordstrom90}, with extensional equality. Universes are not
33 \item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
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.
40 \item[\thydx{LK}] is classical first-order logic as a sequent calculus.
42 \item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$.
44 \item[\thydx{ILL}] implements intuitionistic linear logic.
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
52 http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
54 Note that this is not necessarily consistent with your local sources!
56 \medskip Do not read this manual before reading \emph{Introduction to
57 Isabelle} and performing some Isabelle proofs. Consult the {\em Reference
58 Manual} for more information on tactics, packages, etc.