penultimate Springer draft
authorlcp
Fri Apr 15 18:43:21 1994 +0200 (1994-04-15)
changeset 32992586a978648
parent 328 2d1b460dbb62
child 330 2fda15dd1e0f
penultimate Springer draft
doc-src/preface.tex
     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}