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