|
1 %title% |
|
2 Isabelle's Logics |
|
3 |
|
4 %body% |
|
5 <h3>What is Isabelle?</h3> |
|
6 |
|
7 Isabelle can be viewed from two main perspectives. On the one hand it |
|
8 may serve as a generic framework for rapid prototyping of deductive |
|
9 systems. On the other hand, major existing logics like |
|
10 <strong>Isabelle/HOL</strong> provide a theorem proving environment |
|
11 ready to use for sizable applications. |
|
12 |
|
13 |
|
14 <h2>Isabelle's Logics</h2> |
|
15 |
|
16 The Isabelle distribution includes a large body of object logics and |
|
17 other examples (see the <a href="library/">Isabelle theory |
|
18 library</a>). |
|
19 |
|
20 <dl> |
|
21 |
|
22 <dt><a href="library/HOL/"><strong>Isabelle/HOL</strong></a><dd> is a |
|
23 version of classical higher-order logic resembling that of the <A |
|
24 HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL |
|
25 System</A>. |
|
26 |
|
27 <dt><a href="library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd> |
|
28 adds Scott's Logic for Computable Functions (domain theory) to HOL. |
|
29 |
|
30 <dt><a href="library/FOL/"><strong>Isabelle/FOL</strong></a><dd> |
|
31 provides basic classical and intuitionistic first-order logic. It is |
|
32 polymorphic. |
|
33 |
|
34 <dt><a href="library/ZF/"><strong>Isabelle/ZF</strong></a><dd> offers |
|
35 a formulation of Zermelo-Fraenkel set theory on top of FOL. |
|
36 |
|
37 </dl> |
|
38 |
|
39 <p> |
|
40 |
|
41 Isabelle/HOL is currently the best developed object logic, including |
|
42 an extensive library of (concrete) mathematics, and various packages |
|
43 for advanced definitional concepts (like (co-)inductive sets and |
|
44 types, well-founded recursion etc.). The distribution also includes |
|
45 some large applications, for example correctness proofs of |
|
46 cryptographic protocols (<a href="library/HOL/Auth/">HOL/Auth</a>) or |
|
47 communication protocols (<a href="library/HOLCF/IOA/">HOLCF/IOA</a>). |
|
48 |
|
49 <p> |
|
50 |
|
51 Isabelle/ZF provides another starting point for applications, with a |
|
52 slightly less developed library. Its definitional packages are |
|
53 similar to those of Isabelle/HOL. Untyped ZF provides more advanced |
|
54 constructions for sets than simply-typed HOL. |
|
55 |
|
56 <p> |
|
57 |
|
58 There are a few minor object logics that may serve as further |
|
59 examples: <a href="library/CTT/">CTT</a> is an extensional version of |
|
60 Martin-Löf's Type Theory, <a href="library/Cube/">Cube</a> is |
|
61 Barendregt's Lambda Cube. There are also some sequent calculus |
|
62 examples under <a href="library/Sequents/">Sequents</a>, including |
|
63 modal and linear logics. Again see the <a href="library/">Isabelle |
|
64 theory library</a> for other examples. |
|
65 |
|
66 |
|
67 <h3>Defining Logics</h3> |
|
68 |
|
69 Logics are not hard-wired into Isabelle, but formulated within |
|
70 Isabelle's meta logic: <strong>Isabelle/Pure</strong>. There are |
|
71 quite a lot of syntactic and deductive tools available in generic |
|
72 Isabelle. Thus defining new logics or extending existing ones |
|
73 basically works as follows: |
|
74 |
|
75 <ol> |
|
76 |
|
77 <li> declare concrete syntax (via mixfix grammar and syntax macros), |
|
78 |
|
79 <li> declare abstract syntax (as higher-order constants), |
|
80 |
|
81 <li> declare inference rules (as meta-logical propositions), |
|
82 |
|
83 <li> instantiate generic automatic proof tools (simplifier, classical |
|
84 tableau prover etc.), |
|
85 |
|
86 <li> manually code special proof procedures (via tacticals or |
|
87 hand-written ML). |
|
88 |
|
89 </ol> |
|
90 |
|
91 The first three steps above are fully declarative and involve no ML |
|
92 programming at all. Thus one already gets a decent deductive |
|
93 environment based on primitive inferences (by employing the built-in |
|
94 mechanisms of Isabelle/Pure, in particular higher-order unification |
|
95 and resolution). |
|
96 |
|
97 For sizable applications some degree of automated reasoning is |
|
98 essential. Instantiating existing tools like the classical tableau |
|
99 prover involves only minimal ML-based setup. One may also write |
|
100 arbitrary proof procedures or even theory extension packages in ML, |
|
101 without breaching system soundness (Isabelle follows the well-known |
|
102 <em>LCF system approach</em> to achieve a secure system). |