--- a/doc-src/preface.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,143 +0,0 @@
-\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).