41 Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover. |
41 Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover. |
42 It has been instantiated to support reasoning in several object-logics: |
42 It has been instantiated to support reasoning in several object-logics: |
43 \begin{itemize} |
43 \begin{itemize} |
44 \item first-order logic, constructive and classical versions |
44 \item first-order logic, constructive and classical versions |
45 \item higher-order logic, similar to that of Gordon's {\sc |
45 \item higher-order logic, similar to that of Gordon's {\sc |
46 hol}~\cite{gordon88a} |
46 hol}~\cite{mgordon-hol} |
47 \item Zermelo-Fraenkel set theory~\cite{suppes72} |
47 \item Zermelo-Fraenkel set theory~\cite{suppes72} |
48 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90} |
48 \item an extensional version of Martin-L\"of's Type Theory~\cite{nordstrom90} |
49 \item the classical first-order sequent calculus, {\sc lk} |
49 \item the classical first-order sequent calculus, {\sc lk} |
50 \item the modal logics $T$, $S4$, and $S43$ |
50 \item the modal logics $T$, $S4$, and $S43$ |
51 \item the Logic for Computable Functions~\cite{paulson87} |
51 \item the Logic for Computable Functions~\cite{paulson87} |
66 including a simple theorem prover. Users must be familiar with logic as |
66 including a simple theorem prover. Users must be familiar with logic as |
67 used in computer science; there are many good |
67 used in computer science; there are many good |
68 texts~\cite{galton90,reeves90}. |
68 texts~\cite{galton90,reeves90}. |
69 |
69 |
70 \index{LCF} |
70 \index{LCF} |
71 {\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an |
71 {\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an |
72 ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows |
72 ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows |
73 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an |
73 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an |
74 abstract type; tactics and tacticals support backward proof. But {\sc lcf} |
74 abstract type; tactics and tacticals support backward proof. But {\sc lcf} |
75 represents object-level rules by functions, while Isabelle represents them |
75 represents object-level rules by functions, while Isabelle represents them |
76 by terms. You may find my other writings~\cite{paulson87,paulson-handbook} |
76 by terms. You may find my other writings~\cite{paulson87,paulson-handbook} |
77 helpful in understanding the relationship between {\sc lcf} and Isabelle. |
77 helpful in understanding the relationship between {\sc lcf} and Isabelle. |
78 |
|
79 Isabelle does not keep a record of inference steps. Each step is checked |
|
80 at run time to ensure that theorems can only be constructed by applying |
|
81 inference rules. An Isabelle proof typically involves hundreds of |
|
82 primitive inferences, and would be unintelligible if displayed. |
|
83 Discarding proofs saves vast amounts of storage. But can Isabelle be |
|
84 trusted? If desired, object-logics can be formalized such that each |
|
85 theorem carries a proof term, which could be checked by another program. |
|
86 Proofs can also be traced. |
|
87 |
78 |
88 \index{Isabelle!release history} Isabelle was first distributed in 1986. |
79 \index{Isabelle!release history} Isabelle was first distributed in 1986. |
89 The 1987 version introduced a higher-order meta-logic with an improved |
80 The 1987 version introduced a higher-order meta-logic with an improved |
90 treatment of quantifiers. The 1988 version added limited polymorphism and |
81 treatment of quantifiers. The 1988 version added limited polymorphism and |
91 support for natural deduction. The 1989 version included a parser and |
82 support for natural deduction. The 1989 version included a parser and |
140 \include{foundations} |
131 \include{foundations} |
141 \include{getting} |
132 \include{getting} |
142 \include{advanced} |
133 \include{advanced} |
143 |
134 |
144 \bibliographystyle{plain} \small\raggedright\frenchspacing |
135 \bibliographystyle{plain} \small\raggedright\frenchspacing |
145 \bibliography{string,atp,funprog,general,logicprog,theory} |
136 \bibliography{string,atp,funprog,general,logicprog,isabelle,theory} |
146 |
137 |
147 \input{intro.ind} |
138 \input{intro.ind} |
148 \end{document} |
139 \end{document} |