src/Doc/preface.tex

+\chapter*{Preface}
+\markboth{Preface}{Preface}   %or Preface ?
+%%\addcontentsline{toc}{chapter}{Preface} 
+
+Most theorem provers support a fixed logic, such as first-order or
+equational logic.  They bring sophisticated proof procedures to bear upon
+the conjectured formula.  The resolution prover Otter~\cite{wos-bledsoe} is
+an impressive example.
+
+{\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each
+support a fixed logic too.  These are higher-order type theories,
+explicitly concerned with computation and capable of expressing
+developments in constructive mathematics.  They are far removed from
+classical first-order logic.
+
+A diverse collection of logics --- type theories, process calculi,
+$\lambda$-calculi --- may be found in the Computer Science literature.
+Such logics require proof support.  Few proof procedures are known for
+them, but the theorem prover can at least automate routine steps.
+
+A {\bf generic} theorem prover is one that supports a variety of logics.
+Some generic provers are noteworthy for their user interfaces
+\cite{dawson90,mural,sawamura92}.  Most of them work by implementing a
+syntactic framework that can express typical inference rules.  Isabelle's
+distinctive feature is its representation of logics within a fragment of
+higher-order logic, called the meta-logic.  The proof theory of
+higher-order logic may be used to demonstrate that the representation is
+correct~\cite{paulson89}.  The approach has much in common with the
+Edinburgh Logical Framework~\cite{harper-jacm} and with
+Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.
+
+An inference rule in Isabelle is a generalized Horn clause.  Rules are
+joined to make proofs by resolving such clauses.  Logical variables in
+goals can be instantiated incrementally.  But Isabelle is not a resolution
+theorem prover like Otter.  Isabelle's clauses are drawn from a richer
+language and a fully automatic search would be impractical.  Isabelle does
+not resolve clauses automatically, but under user direction.  You can
+conduct single-step proofs, use Isabelle's built-in proof procedures, or
+develop new proof procedures using tactics and tacticals.
+
+Isabelle's meta-logic is higher-order, based on the simply typed
+$\lambda$-calculus.  So resolution cannot use ordinary unification, but
+higher-order unification~\cite{huet75}.  This complicated procedure gives
+Isabelle strong support for many logical formalisms involving variable
+binding.
+
+The diagram below illustrates some of the logics distributed with Isabelle.
+These include first-order logic (intuitionistic and classical), the sequent
+calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},
+a version of Constructive Type Theory~\cite{nordstrom90}, several modal
+logics, and a Logic for Computable Functions~\cite{paulson87}.  Several
+experimental logics are being developed, such as linear logic.
+
+\centerline{\epsfbox{gfx/Isa-logics.eps}}
+
+
+\section*{How to read this book}
+Isabelle is a complex system, but beginners can get by with a few commands
+and a basic knowledge of how Isabelle works.  Some knowledge of
+Standard~\ML{} is essential because \ML{} is Isabelle's user interface.
+Advanced Isabelle theorem proving can involve writing \ML{} code, possibly
+with Isabelle's sources at hand.  My book on~\ML{}~\cite{paulson91} covers
+much material connected with Isabelle, including a simple theorem prover.
+
+The Isabelle documentation is divided into three parts, which serve
+distinct purposes:
+\begin{itemize}
+\item {\em Introduction to Isabelle\/} describes the basic features of
+  Isabelle.  This part is intended to be read through.  If you are
+  impatient to get started, you might skip the first chapter, which
+  describes Isabelle's meta-logic in some detail.  The other chapters
+  present on-line sessions of increasing difficulty.  It also explains how
+  to derive rules define theories, and concludes with an extended example:
+  a Prolog interpreter.
+
+\item {\em The Isabelle Reference Manual\/} provides detailed information
+  about Isabelle's facilities, excluding the object-logics.  This part
+  would make boring reading, though browsing might be useful.  Mostly you
+  should use it to locate facts quickly.
+
+\item {\em Isabelle's Object-Logics\/} describes the various logics
+  distributed with Isabelle.  The chapters are intended for reference only;
+  they overlap somewhat so that each chapter can be read in isolation.
+\end{itemize}
+This book should not be read from start to finish.  Instead you might read
+a couple of chapters from {\em Introduction to Isabelle}, then try some
+examples referring to the other parts, return to the {\em Introduction},
+and so forth.  Starred sections discuss obscure matters and may be skipped
+on a first reading.
+
+
+
+\section*{Releases of Isabelle}
+Isabelle was first distributed in 1986.  The 1987 version introduced a
+higher-order meta-logic with an improved treatment of quantifiers.  The
+1988 version added limited polymorphism and support for natural deduction.
+The 1989 version included a parser and pretty printer generator.  The 1992
+version introduced type classes, to support many-sorted and higher-order
+logics.  The 1993 version provides greater support for theories and is
+much faster.  
+
+Isabelle is still under development.  Projects under consideration include
+better support for inductive definitions, some means of recording proofs, a
+graphical user interface, and developments in the standard object-logics.
+I hope but cannot promise to maintain upwards compatibility.
+
+Isabelle can be downloaded from .
+\begin{quote}
+{\tt http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/}  
+\end{quote}
+The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk}
+provides a forum for discussing problems and applications involving
+Isabelle.  To join, send me a message via {\tt lcp\at cl.cam.ac.uk}.
+Please notify me of any errors you find in this book.
+
+\section*{Acknowledgements} 
+Tobias Nipkow has made immense contributions to Isabelle, including the
+parser generator, type classes, the simplifier, and several object-logics.
+He also arranged for several of his students to help.  Carsten Clasohm
+implemented the theory database; Markus Wenzel implemented macros; Sonia
+Mahjoub and Karin Nimmermann also contributed.  
+
+Nipkow and his students wrote much of the documentation underlying this
+book.  Nipkow wrote the first versions of \S\ref{sec:defining-theories},
+\S\ref{sec:ref-defining-theories}, Chap.\ts\ref{Defining-Logics},
+Chap.\ts\ref{simp-chap} and App.\ts\ref{app:TheorySyntax}\@.  Carsten
+Clasohm contributed to Chap.\ts\ref{theories}.  Markus Wenzel contributed
+to Chap.\ts\ref{chap:syntax}.  Nipkow also provided the quotation at
+the front.
+
+David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert
+V{\"o}lker and Markus Wenzel suggested changes and corrections to the
+documentation.
+
+Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped
+to develop Isabelle's standard object-logics.  David Aspinall performed
+some useful research into theories and implemented an Isabelle Emacs mode.
+Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,
+Poly/{\sc ml}.  
+
+The research has been funded by numerous SERC grants dating from the Alvey
+programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects
+3245: Logical Frameworks and 6453: Types).