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