| author | wenzelm |
| Tue, 13 Jun 2006 23:41:59 +0200 | |
| changeset 19883 | d064712bdd1d |
| parent 17665 | 64e5aecbf7fd |
| permissions | -rw-r--r-- |
| 16233 | 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"> |
|
| 16240 | 3 |
<!-- $Id$ --> |
| 16233 | 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= |
|
| 17563 | 27 |
"//dist/library/index.html">Isabelle theory library</a>).</p> |
| 16233 | 28 |
|
29 |
<dl> |
|
|
17665
64e5aecbf7fd
removed link to HOL4, which is not in the library right now;
wenzelm
parents:
17563
diff
changeset
|
30 |
<dt id="isabelle_hol"><a |
|
64e5aecbf7fd
removed link to HOL4, which is not in the library right now;
wenzelm
parents:
17563
diff
changeset
|
31 |
href="//dist/library/HOL/index.html">Isabelle/HOL</a></dt> |
|
64e5aecbf7fd
removed link to HOL4, which is not in the library right now;
wenzelm
parents:
17563
diff
changeset
|
32 |
<dd>is a version of classical higher-order logic resembling |
|
64e5aecbf7fd
removed link to HOL4, which is not in the library right now;
wenzelm
parents:
17563
diff
changeset
|
33 |
that of the <a |
|
64e5aecbf7fd
removed link to HOL4, which is not in the library right now;
wenzelm
parents:
17563
diff
changeset
|
34 |
href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL |
|
64e5aecbf7fd
removed link to HOL4, which is not in the library right now;
wenzelm
parents:
17563
diff
changeset
|
35 |
System</a>.</dd> |
| 16233 | 36 |
|
37 |
<dt><a href= |
|
| 17563 | 38 |
"//dist/library/HOLCF/index.html">Isabelle/HOLCF</a></dt> |
| 16233 | 39 |
<dd>adds Scott's Logic for Computable Functions (domain theory) to |
40 |
HOL.</dd> |
|
41 |
||
| 17563 | 42 |
<dt><a href="//dist/library/FOL/index.html">Isabelle/FOL</a></dt> |
| 16233 | 43 |
<dd>provides basic classical and intuitionistic first-order logic. It is |
44 |
polymorphic.</dd> |
|
45 |
||
| 17563 | 46 |
<dt><a href="//dist/library/ZF/index.html">Isabelle/ZF</a></dt> |
| 16233 | 47 |
<dd>offers a formulation of Zermelo-Fraenkel set theory on top of FOL.</dd> |
48 |
</dl> |
|
49 |
||
50 |
<p><em>Isabelle/HOL</em> is currently the best developed object logic, including an |
|
51 |
extensive library of (concrete) mathematics, and various packages for |
|
52 |
advanced definitional concepts like (co-)inductive sets and types, |
|
53 |
well-founded recursion etc. The distribution also includes some large |
|
54 |
applications, for example correctness proofs of cryptographic protocols |
|
| 17563 | 55 |
(<a href="//dist/library/HOL/Auth/index.html">HOL/Auth</a>) or communication |
56 |
protocols (<a href="//dist/library/HOLCF/IOA/index.html">HOLCF/IOA</a>).</p> |
|
| 16233 | 57 |
|
58 |
<p><em>Isabelle/ZF</em> provides another starting point for applications, with a |
|
59 |
slightly less developed library. Its definitional packages are similar to |
|
60 |
those of Isabelle/HOL. Untyped ZF provides more advanced constructions for |
|
61 |
sets than simply-typed HOL.</p> |
|
62 |
||
63 |
<p>There are a few minor object logics that may serve as further examples: |
|
| 17563 | 64 |
<a href="//dist/library/CTT/index.html">CTT</a> is an extensional version of |
65 |
Martin-Löf's Type Theory, <a href="//dist/library/Cube/index.html">Cube</a> is |
|
| 16233 | 66 |
Barendregt's Lambda Cube. There are also some sequent calculus examples under |
| 17563 | 67 |
<a href="//dist/library/Sequents/index.html">Sequents</a>, including modal and |
68 |
linear logics. Again see the <a href="//dist/library/index.html">Isabelle theory |
|
| 16233 | 69 |
library</a> for other examples.</p> |
70 |
||
71 |
<h2>Defining Logics</h2> |
|
72 |
||
73 |
<p>Logics are not hard-wired into Isabelle, but |
|
74 |
formulated within Isabelle's meta logic: <em>Isabelle/Pure</em>. |
|
75 |
There are quite a lot of syntactic and deductive tools available in generic |
|
76 |
Isabelle. Thus defining new logics or extending existing ones basically works |
|
77 |
as follows:</p> |
|
78 |
||
79 |
<ol> |
|
80 |
<li>declare concrete syntax (via mixfix grammar and syntax macros)</li> |
|
81 |
<li>declare abstract syntax (as higher-order constants)</li> |
|
82 |
<li>declare inference rules (as meta-logical propositions)</li> |
|
83 |
<li>instantiate generic automatic proof tools (simplifier, classical |
|
84 |
tableau prover etc.)</li> |
|
85 |
<li>manually code special proof procedures (via tacticals or hand-written |
|
86 |
ML)</li> |
|
87 |
</ol> |
|
88 |
||
89 |
<p>The first three steps above are fully declarative and involve no ML |
|
90 |
programming at all. Thus one already gets a decent deductive environment |
|
91 |
based on primitive inferences (by employing the built-in mechanisms of |
|
92 |
<em>Isabelle/Pure</em>, in particular higher-order unification and resolution). For |
|
93 |
sizable applications some degree of automated reasoning is essential. |
|
94 |
Instantiating existing tools like the classical tableau prover involves only |
|
95 |
minimal ML-based setup. One may also write arbitrary proof procedures or even |
|
| 16272 | 96 |
theory extension packages in ML, without breaking system soundness (Isabelle |
| 16233 | 97 |
follows the well-known <em>LCF system approach</em> to achieve a secure |
98 |
system).</p> |
|
99 |
</div> |
|
100 |
<div class="hr"><hr/></div> |
|
101 |
<?include file="//include/footer.include.html"?> |
|
102 |
</body> |
|
103 |
||
104 |
</html> |