summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/preface.tex

author | wenzelm |

Wed, 15 Apr 2009 11:14:48 +0200 | |

changeset 30895 | bad26d8f0adf |

parent 9695 | ec7d7f877712 |

child 42637 | 381fdcab0f36 |

permissions | -rw-r--r-- |

updated for Isabelle2009;

%% $Id$ \chapter*{Preface} Several logics come with Isabelle. Many of them are sufficiently developed to serve as comfortable reasoning environments. They are also good starting points for defining new logics. Each logic is distributed with sample proofs, some of which are described in this document. \texttt{HOL} is currently the best developed Isabelle object-logic, including an extensive library of (concrete) mathematics, and various packages for advanced definitional concepts (like (co-)inductive sets and types, well-founded recursion etc.). The distribution also includes some large applications. See the separate manual \emph{Isabelle's Logics: HOL}. There is also a comprehensive tutorial on Isabelle/HOL available. \texttt{ZF} provides another starting point for applications, with a slightly less developed library than \texttt{HOL}. \texttt{ZF}'s definitional packages are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides more advanced constructions for sets than simply-typed \texttt{HOL}. \texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}. \medskip There are some further logics distributed with Isabelle: \begin{ttdescription} \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic, which is the basis of a preliminary method for deriving programs from proofs~\cite{coen92}. It is built upon classical~FOL. \item[\thydx{LCF}] is a version of Scott's Logic for Computable Functions, which is also implemented by the~{\sc lcf} system~\cite{paulson87}. It is built upon classical~FOL. \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}. \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type Theory~\cite{nordstrom90}, with extensional equality. Universes are not included. \item[\thydx{Cube}] is Barendregt's $\lambda$-cube. \end{ttdescription} The directory \texttt{Sequents} contains several logics based upon the sequent calculus. Sequents have the form $A@1,\ldots,A@m\turn B@1,\ldots,B@n$; rules are applied using associative matching. \begin{ttdescription} \item[\thydx{LK}] is classical first-order logic as a sequent calculus. \item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$. \item[\thydx{ILL}] implements intuitionistic linear logic. \end{ttdescription} The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt Cube} are undocumented. All object-logics' sources are distributed with Isabelle (see the directory \texttt{src}). They are also available for browsing on the WWW at \begin{center}\small \begin{tabular}{l} \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ \url{http://isabelle.in.tum.de/library/} \\ \end{tabular} \end{center} Note that this is not necessarily consistent with your local sources! \medskip Do not read the \emph{Isabelle's Logics} manuals before reading \emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and performing some Isabelle proofs. Consult the {\em Reference Manual} for more information on tactics, packages, etc. %%% Local Variables: %%% mode: latex %%% TeX-master: "logics" %%% End: