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

doc-src/Logics/preface.tex

changeset 6120 | f40d61cd6b32 |

child 6148 | d97a944c6ea3 |

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/doc-src/Logics/preface.tex Wed Jan 13 16:30:53 1999 +0100 1.3 @@ -0,0 +1,60 @@ 1.4 +%% $Id$ 1.5 +\chapter*{Preface} 1.6 +Several logics come with Isabelle. Many of them are sufficiently developed 1.7 +to serve as comfortable reasoning environments. They are also good 1.8 +starting points for defining new logics. Each logic is distributed with 1.9 +sample proofs, some of which are described in this document. 1.10 + 1.11 +The logics \texttt{FOL} (first-order logic) and \texttt{ZF} (axiomatic set 1.12 +theory) are described in a separate manual~\cite{isabelle-ZF}. Here are the 1.13 +others: 1.14 + 1.15 +\begin{ttdescription} 1.16 +\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic, 1.17 + which is the basis of a preliminary method for deriving programs from 1.18 + proofs~\cite{coen92}. It is built upon classical~\FOL{}. 1.19 + 1.20 +\item[\thydx{LCF}] is a version of Scott's Logic for Computable 1.21 + Functions, which is also implemented by the~{\sc lcf} 1.22 + system~\cite{paulson87}. It is built upon classical~\FOL{}. 1.23 + 1.24 +\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40}, 1.25 +which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}. 1.26 +This object-logic should not be confused with Isabelle's meta-logic, which is 1.27 +also a form of higher-order logic. 1.28 + 1.29 +\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an 1.30 + extension of \texttt{HOL}\@. 1.31 + 1.32 +\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type 1.33 +Theory~\cite{nordstrom90}, with extensional equality. Universes are not 1.34 +included. 1.35 + 1.36 +\item[\thydx{Cube}] is Barendregt's $\lambda$-cube. 1.37 + \end{ttdescription} 1.38 + 1.39 +The directory \texttt{Sequents} contains several logics based 1.40 + upon the sequent calculus. Sequents have the form $A@1,\ldots,A@m\turn 1.41 +B@1,\ldots,B@n$; rules are applied using associative matching. 1.42 +\begin{ttdescription} 1.43 +\item[\thydx{LK}] is classical first-order logic as a sequent calculus. 1.44 + 1.45 +\item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$. 1.46 + 1.47 +\item[\thydx{ILL}] implements intuitionistic linear logic. 1.48 +\end{ttdescription} 1.49 + 1.50 +The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt 1.51 + Cube} are undocumented. All object-logics' sources are 1.52 +distributed with Isabelle (see the directory \texttt{src}). They are 1.53 +also available for browsing on the WWW at 1.54 +\begin{ttbox} 1.55 +http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/ 1.56 +\end{ttbox} 1.57 +Note that this is not necessarily consistent with your local sources! 1.58 + 1.59 +\medskip Do not read this manual before reading \emph{Introduction to 1.60 + Isabelle} and performing some Isabelle proofs. Consult the {\em Reference 1.61 + Manual} for more information on tactics, packages, etc. 1.62 + 1.63 +