|
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=
|
|
|
27 |
"library/index.html">Isabelle theory library</a>).</p>
|
|
|
28 |
|
|
|
29 |
<dl>
|
|
16575
|
30 |
<dt id="isabelle_hol"><a href="//library/HOL/index.html">Isabelle/HOL</a></dt>
|
|
16233
|
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 |
|
|
16575
|
41 |
<dt><a href="//library/FOL/index.html">Isabelle/FOL</a></dt>
|
|
16233
|
42 |
<dd>provides basic classical and intuitionistic first-order logic. It is
|
|
|
43 |
polymorphic.</dd>
|
|
|
44 |
|
|
16575
|
45 |
<dt><a href="//library/ZF/index.html">Isabelle/ZF</a></dt>
|
|
16233
|
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
|
|
16575
|
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>
|
|
16233
|
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:
|
|
16575
|
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
|
|
16233
|
65 |
Barendregt's Lambda Cube. There are also some sequent calculus examples under
|
|
16575
|
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
|
|
16233
|
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
|
|
16272
|
95 |
theory extension packages in ML, without breaking system soundness (Isabelle
|
|
16233
|
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>
|