author haftmann
Wed Dec 27 19:10:06 2006 +0100 (2006-12-27)
changeset 21915 4e63c55f4cb4
parent 9695 ec7d7f877712
child 42637 381fdcab0f36
permissions -rw-r--r--
different handling of type variable names
     1 %% $Id$
     2 \chapter*{Preface}
     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 \texttt{HOL} is currently the best developed Isabelle object-logic, including
     9 an extensive library of (concrete) mathematics, and various packages for
    10 advanced definitional concepts (like (co-)inductive sets and types,
    11 well-founded recursion etc.). The distribution also includes some large
    12 applications.  See the separate manual \emph{Isabelle's Logics: HOL}.  There
    13 is also a comprehensive tutorial on Isabelle/HOL available.
    15 \texttt{ZF} provides another starting point for applications, with a slightly
    16 less developed library than \texttt{HOL}.  \texttt{ZF}'s definitional packages
    17 are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides
    18 more advanced constructions for sets than simply-typed \texttt{HOL}.
    19 \texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described
    20 in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}.
    22 \medskip There are some further logics distributed with Isabelle:
    23 \begin{ttdescription}
    24 \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
    25   which is the basis of a preliminary method for deriving programs from
    26   proofs~\cite{coen92}.  It is built upon classical~FOL.
    28 \item[\thydx{LCF}] is a version of Scott's Logic for Computable
    29   Functions, which is also implemented by the~{\sc lcf}
    30   system~\cite{paulson87}.  It is built upon classical~FOL.
    32 \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
    33   \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}.
    35 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
    36 Theory~\cite{nordstrom90}, with extensional equality.  Universes are not
    37 included.
    39 \item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
    40  \end{ttdescription}
    42 The directory \texttt{Sequents} contains several logics based
    43   upon the sequent calculus.  Sequents have the form $A@1,\ldots,A@m\turn
    44 B@1,\ldots,B@n$; rules are applied using associative matching.
    45 \begin{ttdescription}
    46 \item[\thydx{LK}] is classical first-order logic as a sequent calculus.
    48 \item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$.  
    50 \item[\thydx{ILL}] implements intuitionistic linear logic.
    51 \end{ttdescription}
    53 The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt
    54   Cube} are undocumented.  All object-logics' sources are distributed with
    55 Isabelle (see the directory \texttt{src}).  They are also available for
    56 browsing on the WWW at
    58 \begin{center}\small
    59   \begin{tabular}{l}
    60     \url{} \\
    61     \url{} \\
    62   \end{tabular}
    63 \end{center}
    65 Note that this is not necessarily consistent with your local sources!
    67 \medskip Do not read the \emph{Isabelle's Logics} manuals before reading
    68 \emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and
    69 performing some Isabelle proofs.  Consult the {\em Reference Manual} for more
    70 information on tactics, packages, etc.
    73 %%% Local Variables: 
    74 %%% mode: latex
    75 %%% TeX-master: "logics"
    76 %%% End: