80 extensional version of Martin-Löf's Type Theory, <a |
80 extensional version of Martin-Löf's Type Theory, <a |
81 href="http://www.in.tum.de/~isabelle/library/Cube/">Cube</a> is |
81 href="http://www.in.tum.de/~isabelle/library/Cube/">Cube</a> is |
82 Barendregt's Lambda Cube. There are also some sequent calculus |
82 Barendregt's Lambda Cube. There are also some sequent calculus |
83 examples under <a |
83 examples under <a |
84 href="http://www.in.tum.de/~isabelle/library/Sequents/">Sequents</a>, |
84 href="http://www.in.tum.de/~isabelle/library/Sequents/">Sequents</a>, |
85 including modal or linear logics. There are a few more examples, |
85 including modal or linear logics. Again see the <a |
86 again see the <a |
|
87 href="http://www.in.tum.de/~isabelle/library/">Isabelle theory |
86 href="http://www.in.tum.de/~isabelle/library/">Isabelle theory |
88 library</a>. |
87 library</a> for other examples. |
89 |
88 |
90 |
89 |
91 <h2>Defining Logics</h2> |
90 <h2>Defining Logics</h2> |
92 |
91 |
93 Logics are not hard-wired into Isabelle, but formulated within |
92 Logics are not hard-wired into Isabelle, but formulated within |
105 <li> declare inference rules (as meta-logical propositions), |
104 <li> declare inference rules (as meta-logical propositions), |
106 |
105 |
107 <li> instantiate generic proof tools (simplifier, classical tableau |
106 <li> instantiate generic proof tools (simplifier, classical tableau |
108 prover etc.), |
107 prover etc.), |
109 |
108 |
110 <li> manually code special proof procedures (via tacticals or hand |
109 <li> manually code special proof procedures (via tacticals or |
111 written ML). |
110 hand-written ML). |
112 |
111 |
113 </ol> |
112 </ol> |
114 |
113 |
115 The first 3 steps above are fully declarative and involve no ML |
114 The first 3 steps above are fully declarative and involve no ML |
116 programming at all. Thus one already gets a decent deductive |
115 programming at all. Thus one already gets a decent deductive |
121 For sizable applications some degree of automated reasoning is |
120 For sizable applications some degree of automated reasoning is |
122 essential. Instantiating existing tools like the classical tableau |
121 essential. Instantiating existing tools like the classical tableau |
123 prover involves only minimal ML-based setup. One may also write |
122 prover involves only minimal ML-based setup. One may also write |
124 arbitrary proof procedures or even theory extension packages in ML, |
123 arbitrary proof procedures or even theory extension packages in ML, |
125 without breaching system soundness (Isabelle follows the well-known |
124 without breaching system soundness (Isabelle follows the well-known |
126 "LCF system approach" to achieve a secure system). |
125 <em>LCF system approach</em> to achieve a secure system). |
127 |
126 |
128 |
127 |
129 <h2>Further information</h2> |
128 <h2>Further information</h2> |
130 |
129 |
131 <a href="http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"><img |
130 <a href="http://www.cl.cam.ac.uk/Research/HVG/cambridge.html"><img |
132 src="cambridge.gif" width=144 align=right alt="[Cambridge]"></a> <a |
131 src="cambridge.gif" width=144 align=right alt="[Cambridge]"></a> <a |
133 href="http://www.in.tum.de/~isabelle/"><img src="munich.gif" width=47 |
132 href="http://www.in.tum.de/~isabelle/munich.html"><img |
134 align=right alt="[Munich]"></a> The local Isabelle pages at <a |
133 src="munich.gif" width=47 align=right alt="[Munich]"></a> The local |
135 href="http://www.cl.cam.ac.uk/Research/HVG/isabelle.html">Cambridge</a> |
134 Isabelle pages at <a |
136 and <a href="http://www.in.tum.de/~isabelle/">Munich</a> provide |
135 href="http://www.cl.cam.ac.uk/Research/HVG/cambridge.html">Cambridge</a> |
137 further information on Isabelle and related projects. |
136 and <a href="http://www.in.tum.de/~isabelle/munich.html">Munich</a> |
|
137 provide further information on Isabelle and related projects. |
138 |
138 |
139 </html> |
139 </html> |