author | lcp |

Fri Apr 15 18:43:21 1994 +0200 (1994-04-15) | |

changeset 329 | 92586a978648 |

parent 328 | 2d1b460dbb62 |

child 330 | 2fda15dd1e0f |

penultimate Springer draft

1.1 --- a/doc-src/preface.tex Fri Apr 15 18:34:26 1994 +0200 1.2 +++ b/doc-src/preface.tex Fri Apr 15 18:43:21 1994 +0200 1.3 @@ -2,20 +2,23 @@ 1.4 \markboth{Preface}{Preface} %or Preface ? 1.5 \addcontentsline{toc}{chapter}{Preface} 1.6 1.7 -\index{Isabelle!object-logics supported} 1.8 - 1.9 Most theorem provers support a fixed logic, such as first-order or 1.10 equational logic. They bring sophisticated proof procedures to bear upon 1.11 the conjectured formula. The resolution prover Otter~\cite{wos-bledsoe} is 1.12 -an impressive example. ALF~\cite{alf}, Coq~\cite{coq} and 1.13 -Nuprl~\cite{constable86} each support a fixed logic too, but one far 1.14 -removed from first-order logic. They are explicitly concerned with 1.15 -computation. A diverse collection of logics --- type theories, process 1.16 -calculi, $\lambda$-calculi --- may be found in the Computer Science 1.17 -literature. Such logics require proof support. Few proof procedures are 1.18 -known for them, but the theorem prover can at least automate routine steps. 1.19 +an impressive example. 1.20 1.21 -A {\bf generic} theorem prover is one that can support a variety of logics. 1.22 +{\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each 1.23 +support a fixed logic too. These are higher-order type theories, 1.24 +explicitly concerned with computation and capable of expressing 1.25 +developments in constructive mathematics. They are far removed from 1.26 +classical first-order logic. 1.27 + 1.28 +A diverse collection of logics --- type theories, process calculi, 1.29 +$\lambda$-calculi --- may be found in the Computer Science literature. 1.30 +Such logics require proof support. Few proof procedures are known for 1.31 +them, but the theorem prover can at least automate routine steps. 1.32 + 1.33 +A {\bf generic} theorem prover is one that supports a variety of logics. 1.34 Some generic provers are noteworthy for their user interfaces 1.35 \cite{dawson90,mural,sawamura92}. Most of them work by implementing a 1.36 syntactic framework that can express typical inference rules. Isabelle's 1.37 @@ -35,7 +38,7 @@ 1.38 conduct single-step proofs, use Isabelle's built-in proof procedures, or 1.39 develop new proof procedures using tactics and tacticals. 1.40 1.41 -Isabelle's meta-logic is higher-order, based on the typed 1.42 +Isabelle's meta-logic is higher-order, based on the simply typed 1.43 $\lambda$-calculus. So resolution cannot use ordinary unification, but 1.44 higher-order unification~\cite{huet75}. This complicated procedure gives 1.45 Isabelle strong support for many logical formalisms involving variable 1.46 @@ -45,9 +48,8 @@ 1.47 These include first-order logic (intuitionistic and classical), the sequent 1.48 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72}, 1.49 a version of Constructive Type Theory~\cite{nordstrom90}, several modal 1.50 -logics, and a Logic for Computable Functions. Several experimental 1.51 -logics are also available, such a term assignment calculus for linear 1.52 -logic. 1.53 +logics, and a Logic for Computable Functions. Several experimental logics 1.54 +are being developed, such as linear logic. 1.55 1.56 \centerline{\epsfbox{Isa-logics.eps}} 1.57 1.58 @@ -77,8 +79,8 @@ 1.59 should use it to locate facts quickly. 1.60 1.61 \item {\em Isabelle's Object-Logics\/} describes the various logics 1.62 - distributed with Isabelle. Its final chapter explains how to define new 1.63 - logics. The other chapters are intended for reference only. 1.64 + distributed with Isabelle. The chapters are intended for reference only; 1.65 + they overlap somewhat so that each chapter can be read in isolation. 1.66 \end{itemize} 1.67 This book should not be read from start to finish. Instead you might read 1.68 a couple of chapters from {\em Introduction to Isabelle}, then try some 1.69 @@ -88,7 +90,7 @@ 1.70 1.71 1.72 1.73 -\section*{Releases of Isabelle}\index{Isabelle!release history} 1.74 +\section*{Releases of Isabelle} 1.75 Isabelle was first distributed in 1986. The 1987 version introduced a 1.76 higher-order meta-logic with an improved treatment of quantifiers. The 1.77 1988 version added limited polymorphism and support for natural deduction. 1.78 @@ -125,13 +127,15 @@ 1.79 1.80 Nipkow and his students wrote much of the documentation underlying this 1.81 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories}, 1.82 -\S\ref{sec:ref-defining-theories}, Chap.\ts\ref{simp-chap}, 1.83 -Chap.\ts\ref{Defining-Logics} and App.\ts\ref{app:TheorySyntax}\@. Carsten 1.84 +\S\ref{sec:ref-defining-theories}, Chap.\ts\ref{Defining-Logics}, 1.85 +Chap.\ts\ref{simp-chap} and App.\ts\ref{app:TheorySyntax}\@. Carsten 1.86 Clasohm contributed to Chap.\ts\ref{theories}. Markus Wenzel contributed 1.87 -to Chap.\ts\ref{Defining-Logics}. 1.88 +to Chap.\ts\ref{chap:syntax}. Nipkow also provided the quotation at 1.89 +the front. 1.90 1.91 -David Aspinall, Sara Kalvala, Ina Kraan, Zhenyu Qian, Norbert V{\"o}lker and 1.92 -Markus Wenzel suggested changes and corrections to the documentation. 1.93 +David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert 1.94 +V{\"o}lker and Markus Wenzel suggested changes and corrections to the 1.95 +documentation. 1.96 1.97 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped 1.98 to develop Isabelle's standard object-logics. David Aspinall performed 1.99 @@ -142,6 +146,3 @@ 1.100 The research has been funded by numerous SERC grants dating from the Alvey 1.101 programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects 1.102 3245: Logical Frameworks and 6453: Types). 1.103 - 1.104 - 1.105 -\index{ML}