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