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