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 objectlogic, 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 
wellfounded 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 simplytyped \texttt{HOL}.

wenzelm@6582

18 
\texttt{ZF} is built on \texttt{FOL} (firstorder logic), both are described

wenzelm@6582

19 
in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelleZF}.

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 MartinL\"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 firstorder 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 objectlogics' 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 
%%% TeXmaster: "logics"

wenzelm@6148

75 
%%% End:
