|
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>Overview</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>What is Isabelle?</h2>
|
|
|
18 |
<p>
|
|
|
19 |
Isabelle is a generic proof assistant. It allows mathematical
|
|
|
20 |
formulas to be expressed in a formal language and provides tools
|
|
|
21 |
for proving those formulas in a logical calculus. The main
|
|
|
22 |
application is the formalization of mathematical proofs and in
|
|
|
23 |
particular <em>formal verification</em>, which includes proving
|
|
|
24 |
the correctness of computer hardware or software and proving
|
|
|
25 |
properties of computer languages and protocols.</p>
|
|
|
26 |
|
|
|
27 |
<p>Compared with similar tools, Isabelle's distinguishing feature is its
|
|
|
28 |
flexibility. Most proof assistants are built around a single formal calculus,
|
|
|
29 |
typically higher-order logic. Isabelle has the capacity to accept a variety
|
|
|
30 |
of formal calculi. The distributed version supports higher-order logic but
|
|
|
31 |
also axiomatic set theory and several other formalisms. See
|
|
|
32 |
<a href="logics.html">logics</a> for more details.</p>
|
|
|
33 |
|
|
|
34 |
<p>Isabelle is a joint project between Lawrence C. Paulson
|
|
|
35 |
(University of Cambridge, UK) and Tobias Nipkow (Technical
|
|
|
36 |
University of Munich, Germany).</p>
|
|
|
37 |
|
|
16416
|
38 |
<h2>Preview of Isabelle</h2>
|
|
16233
|
39 |
|
|
16296
|
40 |
<a href="//media/pg_preview.mov">
|
|
16233
|
41 |
<img class="left" src="//img/isabelle_pg_screenshot_small.png" alt="Sreenshot "
|
|
|
42 |
width="250" height="277" />
|
|
|
43 |
</a>
|
|
|
44 |
|
|
16296
|
45 |
<p>Here is a <a href="//media/pg_preview.mov">hyperlinked preview</a> demonstrating
|
|
|
46 |
Isabelle and ProofGeneral, in <a href="http://www.apple.com/quicktime/download/">QuickTime
|
|
|
47 |
format</a>, and also as a <a href="//media/pg_preview.pdf">non-hyperlinked preview</a> in PDF.</p>
|
|
|
48 |
<br clear="all"/>
|
|
|
49 |
|
|
|
50 |
<h2>What Isabelle offers</h2>
|
|
|
51 |
|
|
16233
|
52 |
<p>Isabelle provides excellent notational support: new notations
|
|
|
53 |
can be introduced, using normal mathematical symbols. Proofs can
|
|
|
54 |
be written in a structured notation based upon traditional proof
|
|
|
55 |
style, or more straightforwardly as sequences of
|
|
|
56 |
commands. Definitions and proofs may include TeX source, from
|
|
|
57 |
which Isabelle can automatically generate typeset documents.</p>
|
|
|
58 |
|
|
|
59 |
<p>The main limitation of all such proof systems is that proving
|
|
|
60 |
theorems requires much effort from an expert user. Isabelle
|
|
|
61 |
incorporates some tools to improve the user's productivity by
|
|
|
62 |
automating some parts of the proof process. In particular,
|
|
|
63 |
Isabelle's <em>classical reasoner</em> can perform long chains
|
|
|
64 |
of reasoning steps to prove formulas. The <em>simplifier</em>
|
|
|
65 |
can reason with and about equations. Linear <em>arithmetic</em>
|
|
|
66 |
facts are proved automatically.</p>
|
|
|
67 |
|
|
|
68 |
<p>Isabelle comes with a large theory library of formally
|
|
|
69 |
verified mathematics, including elementary number theory (for
|
|
|
70 |
example, Gauss's law of quadratic reciprocity), analysis (basic
|
|
|
71 |
properties of limits, derivatives and integrals), algebra (up to
|
|
|
72 |
Sylow's theorem) and set theory (the relative consistency of the
|
|
|
73 |
Axiom of Choice). Also provided are numerous examples arising
|
|
|
74 |
from research into formal verification.</p>
|
|
|
75 |
|
|
|
76 |
<p>With <em>Isar</em>, Isabelle offers a concise proof formulation language
|
|
|
77 |
which enables a user to write proof scripts naturally understandable for
|
|
|
78 |
both humans <em>and</em> computers.</p>
|
|
|
79 |
|
|
|
80 |
<p>Isabelle is closely integrated with the <a href=
|
|
|
81 |
"http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> user interface, which
|
|
|
82 |
eases the task of writing and maintaining proof scripts.</p>
|
|
16240
|
83 |
<br clear="all" />
|
|
16233
|
84 |
|
|
|
85 |
<p>Ample <a href="dist/documentation.html">documentation</a> is available
|
|
|
86 |
about using Isabelle and its inner concepts, including a
|
|
|
87 |
<a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
|
|
|
88 |
Springer-Verlag.</p>
|
|
16296
|
89 |
|
|
16233
|
90 |
<h2>Projects</h2>
|
|
|
91 |
|
|
|
92 |
<p>There is an (incomplete) list of past and present <a href=
|
|
|
93 |
"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a>
|
|
|
94 |
undertaken using Isabelle available.</p>
|
|
|
95 |
|
|
|
96 |
<h2>License</h2>
|
|
|
97 |
|
|
|
98 |
<p>Isabelle is distributed free of charge under the open source
|
|
16284
|
99 |
<!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD license<!--/a-->. You may use any of our <a
|
|
16233
|
100 |
href="dist/index.html">mirrors</a> for download.</p>
|
|
|
101 |
|
|
|
102 |
</div>
|
|
|
103 |
<div class="hr"><hr/></div>
|
|
|
104 |
<?include file="//include/footer.include.html"?>
|
|
|
105 |
</body>
|
|
|
106 |
|
|
|
107 |
</html>
|