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