doc-src/preface.tex
author nipkow
Mon Jan 29 22:25:45 2001 +0100 (2001-01-29)
changeset 10995 ef0b521698b7
parent 5374 6ef3742b6153
child 14379 ea10a8c3e9cf
permissions -rw-r--r--
*** empty log message ***
     1 \chapter*{Preface}
     2 \markboth{Preface}{Preface}   %or Preface ?
     3 %%\addcontentsline{toc}{chapter}{Preface} 
     4 
     5 Most theorem provers support a fixed logic, such as first-order or
     6 equational logic.  They bring sophisticated proof procedures to bear upon
     7 the conjectured formula.  The resolution prover Otter~\cite{wos-bledsoe} is
     8 an impressive example.
     9 
    10 {\sc alf}~\cite{alf}, Coq~\cite{coq} and Nuprl~\cite{constable86} each
    11 support a fixed logic too.  These are higher-order type theories,
    12 explicitly concerned with computation and capable of expressing
    13 developments in constructive mathematics.  They are far removed from
    14 classical first-order logic.
    15 
    16 A diverse collection of logics --- type theories, process calculi,
    17 $\lambda$-calculi --- may be found in the Computer Science literature.
    18 Such logics require proof support.  Few proof procedures are known for
    19 them, but the theorem prover can at least automate routine steps.
    20 
    21 A {\bf generic} theorem prover is one that supports a variety of logics.
    22 Some generic provers are noteworthy for their user interfaces
    23 \cite{dawson90,mural,sawamura92}.  Most of them work by implementing a
    24 syntactic framework that can express typical inference rules.  Isabelle's
    25 distinctive feature is its representation of logics within a fragment of
    26 higher-order logic, called the meta-logic.  The proof theory of
    27 higher-order logic may be used to demonstrate that the representation is
    28 correct~\cite{paulson89}.  The approach has much in common with the
    29 Edinburgh Logical Framework~\cite{harper-jacm} and with
    30 Felty's~\cite{felty93} use of $\lambda$Prolog to implement logics.
    31 
    32 An inference rule in Isabelle is a generalized Horn clause.  Rules are
    33 joined to make proofs by resolving such clauses.  Logical variables in
    34 goals can be instantiated incrementally.  But Isabelle is not a resolution
    35 theorem prover like Otter.  Isabelle's clauses are drawn from a richer
    36 language and a fully automatic search would be impractical.  Isabelle does
    37 not resolve clauses automatically, but under user direction.  You can
    38 conduct single-step proofs, use Isabelle's built-in proof procedures, or
    39 develop new proof procedures using tactics and tacticals.
    40 
    41 Isabelle's meta-logic is higher-order, based on the simply typed
    42 $\lambda$-calculus.  So resolution cannot use ordinary unification, but
    43 higher-order unification~\cite{huet75}.  This complicated procedure gives
    44 Isabelle strong support for many logical formalisms involving variable
    45 binding.
    46 
    47 The diagram below illustrates some of the logics distributed with Isabelle.
    48 These include first-order logic (intuitionistic and classical), the sequent
    49 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},
    50 a version of Constructive Type Theory~\cite{nordstrom90}, several modal
    51 logics, and a Logic for Computable Functions~\cite{paulson87}.  Several
    52 experimental logics are being developed, such as linear logic.
    53 
    54 \centerline{\epsfbox{gfx/Isa-logics.eps}}
    55 
    56 
    57 \section*{How to read this book}
    58 Isabelle is a complex system, but beginners can get by with a few commands
    59 and a basic knowledge of how Isabelle works.  Some knowledge of
    60 Standard~\ML{} is essential because \ML{} is Isabelle's user interface.
    61 Advanced Isabelle theorem proving can involve writing \ML{} code, possibly
    62 with Isabelle's sources at hand.  My book on~\ML{}~\cite{paulson91} covers
    63 much material connected with Isabelle, including a simple theorem prover.
    64 
    65 The Isabelle documentation is divided into three parts, which serve
    66 distinct purposes:
    67 \begin{itemize}
    68 \item {\em Introduction to Isabelle\/} describes the basic features of
    69   Isabelle.  This part is intended to be read through.  If you are
    70   impatient to get started, you might skip the first chapter, which
    71   describes Isabelle's meta-logic in some detail.  The other chapters
    72   present on-line sessions of increasing difficulty.  It also explains how
    73   to derive rules define theories, and concludes with an extended example:
    74   a Prolog interpreter.
    75 
    76 \item {\em The Isabelle Reference Manual\/} provides detailed information
    77   about Isabelle's facilities, excluding the object-logics.  This part
    78   would make boring reading, though browsing might be useful.  Mostly you
    79   should use it to locate facts quickly.
    80 
    81 \item {\em Isabelle's Object-Logics\/} describes the various logics
    82   distributed with Isabelle.  The chapters are intended for reference only;
    83   they overlap somewhat so that each chapter can be read in isolation.
    84 \end{itemize}
    85 This book should not be read from start to finish.  Instead you might read
    86 a couple of chapters from {\em Introduction to Isabelle}, then try some
    87 examples referring to the other parts, return to the {\em Introduction},
    88 and so forth.  Starred sections discuss obscure matters and may be skipped
    89 on a first reading.
    90 
    91 
    92 
    93 \section*{Releases of Isabelle}
    94 Isabelle was first distributed in 1986.  The 1987 version introduced a
    95 higher-order meta-logic with an improved treatment of quantifiers.  The
    96 1988 version added limited polymorphism and support for natural deduction.
    97 The 1989 version included a parser and pretty printer generator.  The 1992
    98 version introduced type classes, to support many-sorted and higher-order
    99 logics.  The 1993 version provides greater support for theories and is
   100 much faster.  
   101 
   102 Isabelle is still under development.  Projects under consideration include
   103 better support for inductive definitions, some means of recording proofs, a
   104 graphical user interface, and developments in the standard object-logics.
   105 I hope but cannot promise to maintain upwards compatibility.
   106 
   107 Isabelle is available by anonymous ftp:
   108 \begin{itemize}
   109 \item University of Cambridge\\
   110         host {\tt ftp.cl.cam.ac.uk}\\
   111         directory {\tt ml}
   112 
   113 \item Technical University of Munich\\
   114         host {\tt ftp.informatik.tu-muenchen.de}\\
   115         directory {\tt local/lehrstuhl/nipkow}
   116 \end{itemize}
   117 The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk}
   118 provides a forum for discussing problems and applications involving
   119 Isabelle.  To join, send me a message via {\tt lcp\at cl.cam.ac.uk}.
   120 Please notify me of any errors you find in this book.
   121 
   122 \section*{Acknowledgements} 
   123 Tobias Nipkow has made immense contributions to Isabelle, including the
   124 parser generator, type classes, the simplifier, and several object-logics.
   125 He also arranged for several of his students to help.  Carsten Clasohm
   126 implemented the theory database; Markus Wenzel implemented macros; Sonia
   127 Mahjoub and Karin Nimmermann also contributed.  
   128 
   129 Nipkow and his students wrote much of the documentation underlying this
   130 book.  Nipkow wrote the first versions of \S\ref{sec:defining-theories},
   131 \S\ref{sec:ref-defining-theories}, Chap.\ts\ref{Defining-Logics},
   132 Chap.\ts\ref{simp-chap} and App.\ts\ref{app:TheorySyntax}\@.  Carsten
   133 Clasohm contributed to Chap.\ts\ref{theories}.  Markus Wenzel contributed
   134 to Chap.\ts\ref{chap:syntax}.  Nipkow also provided the quotation at
   135 the front.
   136 
   137 David Aspinall, Sara Kalvala, Ina Kraan, Chris Owens, Zhenyu Qian, Norbert
   138 V{\"o}lker and Markus Wenzel suggested changes and corrections to the
   139 documentation.
   140 
   141 Martin Coen, Rajeev Gor\'e, Philippe de Groote and Philippe No\"el helped
   142 to develop Isabelle's standard object-logics.  David Aspinall performed
   143 some useful research into theories and implemented an Isabelle Emacs mode.
   144 Isabelle was developed using Dave Matthews's Standard~{\sc ml} compiler,
   145 Poly/{\sc ml}.  
   146 
   147 The research has been funded by numerous SERC grants dating from the Alvey
   148 programme (grants GR/E0355.7, GR/G53279, GR/H40570) and by ESPRIT (projects
   149 3245: Logical Frameworks and 6453: Types).