doc-src/Logics/preface.tex
changeset 6120 f40d61cd6b32
child 6148 d97a944c6ea3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Logics/preface.tex	Wed Jan 13 16:30:53 1999 +0100
     1.3 @@ -0,0 +1,60 @@
     1.4 +%% $Id$
     1.5 +\chapter*{Preface}
     1.6 +Several logics come with Isabelle.  Many of them are sufficiently developed
     1.7 +to serve as comfortable reasoning environments.  They are also good
     1.8 +starting points for defining new logics.  Each logic is distributed with
     1.9 +sample proofs, some of which are described in this document.
    1.10 +
    1.11 +The logics \texttt{FOL} (first-order logic) and \texttt{ZF} (axiomatic set
    1.12 +theory) are described in a separate manual~\cite{isabelle-ZF}.  Here are the
    1.13 +others:
    1.14 +
    1.15 +\begin{ttdescription}
    1.16 +\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
    1.17 +  which is the basis of a preliminary method for deriving programs from
    1.18 +  proofs~\cite{coen92}.  It is built upon classical~\FOL{}.
    1.19 + 
    1.20 +\item[\thydx{LCF}] is a version of Scott's Logic for Computable
    1.21 +  Functions, which is also implemented by the~{\sc lcf}
    1.22 +  system~\cite{paulson87}.  It is built upon classical~\FOL{}.
    1.23 +
    1.24 +\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40},
    1.25 +which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}.
    1.26 +This object-logic should not be confused with Isabelle's meta-logic, which is
    1.27 +also a form of higher-order logic.
    1.28 +
    1.29 +\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an
    1.30 +  extension of \texttt{HOL}\@.
    1.31 + 
    1.32 +\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
    1.33 +Theory~\cite{nordstrom90}, with extensional equality.  Universes are not
    1.34 +included.
    1.35 +
    1.36 +\item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
    1.37 + \end{ttdescription}
    1.38 +
    1.39 +The directory \texttt{Sequents} contains several logics based
    1.40 +  upon the sequent calculus.  Sequents have the form $A@1,\ldots,A@m\turn
    1.41 +B@1,\ldots,B@n$; rules are applied using associative matching.
    1.42 +\begin{ttdescription}
    1.43 +\item[\thydx{LK}] is classical first-order logic as a sequent calculus.
    1.44 +
    1.45 +\item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$.  
    1.46 +
    1.47 +\item[\thydx{ILL}] implements intuitionistic linear logic.
    1.48 +\end{ttdescription}
    1.49 +
    1.50 +The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt
    1.51 +  Cube} are undocumented.  All object-logics' sources are
    1.52 +distributed with Isabelle (see the directory \texttt{src}).  They are
    1.53 +also available for browsing on the WWW at
    1.54 +\begin{ttbox}
    1.55 +http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
    1.56 +\end{ttbox}
    1.57 +Note that this is not necessarily consistent with your local sources!
    1.58 +
    1.59 +\medskip Do not read this manual before reading \emph{Introduction to
    1.60 +  Isabelle} and performing some Isabelle proofs.  Consult the {\em Reference
    1.61 +  Manual} for more information on tactics, packages, etc.
    1.62 +
    1.63 +