summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/preface.tex

changeset 6582 | 75f31d45fb8b |

parent 6148 | d97a944c6ea3 |

child 6623 | 021728c71030 |

--- a/doc-src/Logics/preface.tex Tue May 04 18:04:45 1999 +0200 +++ b/doc-src/Logics/preface.tex Tue May 04 18:05:34 1999 +0200 @@ -5,10 +5,21 @@ starting points for defining new logics. Each logic is distributed with sample proofs, some of which are described in this document. -The logics \texttt{FOL} (first-order logic) and \texttt{ZF} (axiomatic set -theory) are described in a separate manual~\cite{isabelle-ZF}. Here are the -others: +\texttt{HOL} is currently the best developed Isabelle object-logic, including +an extensive library of (concrete) mathematics, and various packages for +advanced definitional concepts (like (co-)inductive sets and types, +well-founded recursion etc.). The distribution also includes some large +applications. See the separate manual \emph{Isabelle's Logics: HOL}. There +is also a comprehensive tutorial on Isabelle/HOL available. +\texttt{ZF} provides another starting point for applications, with a slightly +less developed library than \texttt{HOL}. \texttt{ZF}'s definitional packages +are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides +more advanced constructions for sets than simply-typed \texttt{HOL}. +\texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described +in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}. + +\medskip There are some further logics distributed with Isabelle: \begin{ttdescription} \item[\thydx{CCL}] is Martin Coen's Classical Computational Logic, which is the basis of a preliminary method for deriving programs from @@ -17,14 +28,9 @@ \item[\thydx{LCF}] is a version of Scott's Logic for Computable Functions, which is also implemented by the~{\sc lcf} system~\cite{paulson87}. It is built upon classical~\FOL{}. - -\item[\thydx{HOL}] is the higher-order logic of Church~\cite{church40}, -which is also implemented by Gordon's~{\sc hol} system~\cite{mgordon-hol}. -This object-logic should not be confused with Isabelle's meta-logic, which is -also a form of higher-order logic. - -\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an - extension of \texttt{HOL}\@. + +\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of + \texttt{HOL}\@. %FIXME See \cite{MNOS98} for more details on \texttt{HOLCF}. \item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type Theory~\cite{nordstrom90}, with extensional equality. Universes are not @@ -44,19 +50,20 @@ \item[\thydx{ILL}] implements intuitionistic linear logic. \end{ttdescription} -The logics \texttt{CCL}, \texttt{LCF}, \texttt{HOLCF}, \texttt{Modal}, \texttt{ILL} and {\tt - Cube} are undocumented. All object-logics' sources are -distributed with Isabelle (see the directory \texttt{src}). They are -also available for browsing on the WWW at +The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt + Cube} are undocumented. All object-logics' sources are distributed with +Isabelle (see the directory \texttt{src}). They are also available for +browsing on the WWW at \begin{ttbox} http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/ http://isabelle.in.tum.de/library/ \end{ttbox} Note that this is not necessarily consistent with your local sources! -\medskip Do not read this manual before reading \emph{Introduction to - Isabelle} and performing some Isabelle proofs. Consult the {\em Reference - Manual} for more information on tactics, packages, etc. +\medskip Do not read the \emph{Isabelle's Logics} manuals before reading +\emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and +performing some Isabelle proofs. Consult the {\em Reference Manual} for more +information on tactics, packages, etc. %%% Local Variables: