summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/Logics/preface.tex

author | haftmann |

Wed Dec 27 19:10:06 2006 +0100 (2006-12-27) | |

changeset 21915 | 4e63c55f4cb4 |

parent 9695 | ec7d7f877712 |

child 42637 | 381fdcab0f36 |

permissions | -rw-r--r-- |

different handling of type variable names

1 %% $Id$

2 \chapter*{Preface}

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

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

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

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

8 \texttt{HOL} is currently the best developed Isabelle object-logic, including

9 an extensive library of (concrete) mathematics, and various packages for

10 advanced definitional concepts (like (co-)inductive sets and types,

11 well-founded recursion etc.). The distribution also includes some large

12 applications. See the separate manual \emph{Isabelle's Logics: HOL}. There

13 is also a comprehensive tutorial on Isabelle/HOL available.

15 \texttt{ZF} provides another starting point for applications, with a slightly

16 less developed library than \texttt{HOL}. \texttt{ZF}'s definitional packages

17 are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides

18 more advanced constructions for sets than simply-typed \texttt{HOL}.

19 \texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described

20 in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}.

22 \medskip There are some further logics distributed with Isabelle:

23 \begin{ttdescription}

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

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

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

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

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

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

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

33 \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}.

35 \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type

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

37 included.

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

40 \end{ttdescription}

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

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

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

45 \begin{ttdescription}

46 \item[\thydx{LK}] is classical first-order logic as a sequent calculus.

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

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

51 \end{ttdescription}

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

54 Cube} are undocumented. All object-logics' sources are distributed with

55 Isabelle (see the directory \texttt{src}). They are also available for

56 browsing on the WWW at

58 \begin{center}\small

59 \begin{tabular}{l}

60 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\

61 \url{http://isabelle.in.tum.de/library/} \\

62 \end{tabular}

63 \end{center}

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

67 \medskip Do not read the \emph{Isabelle's Logics} manuals before reading

68 \emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and

69 performing some Isabelle proofs. Consult the {\em Reference Manual} for more

70 information on tactics, packages, etc.

73 %%% Local Variables:

74 %%% mode: latex

75 %%% TeX-master: "logics"

76 %%% End: