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