equal
deleted
inserted
replaced
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 |