paulson@6120

1 
%% $Id$

paulson@6120

2 
\chapter*{Preface}

paulson@6120

3 
Several logics come with Isabelle. Many of them are sufficiently developed

paulson@6120

4 
to serve as comfortable reasoning environments. They are also good

paulson@6120

5 
starting points for defining new logics. Each logic is distributed with

paulson@6120

6 
sample proofs, some of which are described in this document.

paulson@6120

7 

paulson@6120

8 
The logics \texttt{FOL} (firstorder logic) and \texttt{ZF} (axiomatic set

paulson@6120

9 
theory) are described in a separate manual~\cite{isabelleZF}. Here are the

paulson@6120

10 
others:

paulson@6120

11 

paulson@6120

12 
\begin{ttdescription}

paulson@6120

13 
\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,

paulson@6120

14 
which is the basis of a preliminary method for deriving programs from

paulson@6120

15 
proofs~\cite{coen92}. It is built upon classical~\FOL{}.

paulson@6120

16 

paulson@6120

17 
\item[\thydx{LCF}] is a version of Scott's Logic for Computable

paulson@6120

18 
Functions, which is also implemented by the~{\sc lcf}

paulson@6120

19 
system~\cite{paulson87}. It is built upon classical~\FOL{}.

paulson@6120

20 

paulson@6120

21 
\item[\thydx{HOL}] is the higherorder logic of Church~\cite{church40},

paulson@6120

22 
which is also implemented by Gordon's~{\sc hol} system~\cite{mgordonhol}.

paulson@6120

23 
This objectlogic should not be confused with Isabelle's metalogic, which is

paulson@6120

24 
also a form of higherorder logic.

paulson@6120

25 

paulson@6120

26 
\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an

paulson@6120

27 
extension of \texttt{HOL}\@.

paulson@6120

28 

paulson@6120

29 
\item[\thydx{CTT}] is a version of MartinL\"of's Constructive Type

paulson@6120

30 
Theory~\cite{nordstrom90}, with extensional equality. Universes are not

paulson@6120

31 
included.

paulson@6120

32 

paulson@6120

33 
\item[\thydx{Cube}] is Barendregt's $\lambda$cube.

paulson@6120

34 
\end{ttdescription}

paulson@6120

35 

paulson@6120

36 
The directory \texttt{Sequents} contains several logics based

paulson@6120

37 
upon the sequent calculus. Sequents have the form $A@1,\ldots,A@m\turn

paulson@6120

38 
B@1,\ldots,B@n$; rules are applied using associative matching.

paulson@6120

39 
\begin{ttdescription}

paulson@6120

40 
\item[\thydx{LK}] is classical firstorder logic as a sequent calculus.

paulson@6120

41 

paulson@6120

42 
\item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$.

paulson@6120

43 

paulson@6120

44 
\item[\thydx{ILL}] implements intuitionistic linear logic.

paulson@6120

45 
\end{ttdescription}

paulson@6120

46 

paulson@6120

47 
The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt

paulson@6120

48 
Cube} are undocumented. All objectlogics' sources are

paulson@6120

49 
distributed with Isabelle (see the directory \texttt{src}). They are

paulson@6120

50 
also available for browsing on the WWW at

paulson@6120

51 
\begin{ttbox}

paulson@6120

52 
http://www4.informatik.tumuenchen.de/~nipkow/isabelle/

paulson@6120

53 
\end{ttbox}

paulson@6120

54 
Note that this is not necessarily consistent with your local sources!

paulson@6120

55 

paulson@6120

56 
\medskip Do not read this manual before reading \emph{Introduction to

paulson@6120

57 
Isabelle} and performing some Isabelle proofs. Consult the {\em Reference

paulson@6120

58 
Manual} for more information on tactics, packages, etc.

paulson@6120

59 

paulson@6120

60 
