doc-src/preface.tex
 changeset 356 2e6545875982 parent 329 92586a978648 child 5374 6ef3742b6153
equal inserted replaced
355:77150178beb2 356:2e6545875982
     1 \chapter*{Preface}
     1 \chapter*{Preface}
     2 \markboth{Preface}{Preface}   %or Preface ?
     2 \markboth{Preface}{Preface}   %or Preface ?
     3 \addcontentsline{toc}{chapter}{Preface}
     3 %%\addcontentsline{toc}{chapter}{Preface}
     4
     4
     5 Most theorem provers support a fixed logic, such as first-order or
     5 Most theorem provers support a fixed logic, such as first-order or
     6 equational logic.  They bring sophisticated proof procedures to bear upon
     6 equational logic.  They bring sophisticated proof procedures to bear upon
     7 the conjectured formula.  The resolution prover Otter~\cite{wos-bledsoe} is
     7 the conjectured formula.  The resolution prover Otter~\cite{wos-bledsoe} is
     8 an impressive example.
     8 an impressive example.
    46
    46
    47 The diagram below illustrates some of the logics distributed with Isabelle.
    47 The diagram below illustrates some of the logics distributed with Isabelle.
    48 These include first-order logic (intuitionistic and classical), the sequent
    48 These include first-order logic (intuitionistic and classical), the sequent
    49 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},
    49 calculus, higher-order logic, Zermelo-Fraenkel set theory~\cite{suppes72},
    50 a version of Constructive Type Theory~\cite{nordstrom90}, several modal
    50 a version of Constructive Type Theory~\cite{nordstrom90}, several modal
    51 logics, and a Logic for Computable Functions.  Several experimental logics
    51 logics, and a Logic for Computable Functions~\cite{paulson87}.  Several
    52 are being developed, such as linear logic.
    52 experimental logics are being developed, such as linear logic.
    53
    53
    54 \centerline{\epsfbox{Isa-logics.eps}}
    54 \centerline{\epsfbox{Isa-logics.eps}}
    55
    55
    56
    56
    57 \section*{How to read this book}
    57 \section*{How to read this book}
   112
   112
   113 \item Technical University of Munich\\
   113 \item Technical University of Munich\\
   114         host {\tt ftp.informatik.tu-muenchen.de}\\
   114         host {\tt ftp.informatik.tu-muenchen.de}\\
   115         directory {\tt local/lehrstuhl/nipkow}
   115         directory {\tt local/lehrstuhl/nipkow}
   116 \end{itemize}
   116 \end{itemize}
   117 My electronic mail address is {\tt lcp\at cl.cam.ac.uk}.  Please report any
   117 The electronic distribution list {\tt isabelle-users\at cl.cam.ac.uk}
   118 errors you find in this book and your problems or successes with Isabelle.
   118 provides a forum for discussing problems and applications involving
   119
   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.
   120
   121
   121 \section*{Acknowledgements}
   122 \section*{Acknowledgements}
   122 Tobias Nipkow has made immense contributions to Isabelle, including the
   123 Tobias Nipkow has made immense contributions to Isabelle, including the
   123 parser generator, type classes, the simplifier, and several object-logics.
   124 parser generator, type classes, the simplifier, and several object-logics.
   124 He also arranged for several of his students to help.  Carsten Clasohm
   125 He also arranged for several of his students to help.  Carsten Clasohm