1 %title% |
|
2 Isabelle overview |
|
3 |
|
4 %body% |
|
5 |
|
6 <p> |
|
7 <a href="http://isabelle.in.tum.de/">Isabelle</a> is a generic proof |
|
8 assistant. It allows mathematical formulas to be expressed in a formal |
|
9 language and provides tools for proving those formulas in a logical |
|
10 calculus. The main application is the formalization of mathematical proofs |
|
11 and in particular <em>formal verification</em>, which includes proving the |
|
12 correctness of computer hardware or software and proving properties of |
|
13 computer languages and protocols. |
|
14 </p> |
|
15 |
|
16 <p>Compared with similar tools, Isabelle's distinguishing feature is |
|
17 its flexibility. Most proof assistants are built around a single |
|
18 formal calculus, typically higher-order logic. Isabelle has the |
|
19 capacity to accept a variety of formal calculi. The distributed |
|
20 version supports higher-order logic but also axiomatic set theory and |
|
21 several <a href="logics.html">other formalisms</a>. Isabelle provides |
|
22 excellent notational support: new notations can be introduced, using |
|
23 normal mathematical symbols. Proofs can be written in a structured |
|
24 notation based upon traditional proof style, or more straightforwardly |
|
25 as sequences of commands. Definitions and proofs may include TeX |
|
26 source, from which Isabelle can automatically generate typeset |
|
27 documents.</p> |
|
28 |
|
29 <p>The main limitation of all such systems is that proving theorems |
|
30 requires much effort from an expert user. Isabelle incorporates some |
|
31 tools to improve the user's productivity by automating some parts of |
|
32 the proof process. In particular, Isabelle's <em>classical |
|
33 reasoner</em> can perform long chains of reasoning steps to prove |
|
34 formulas. The <em>simplifier</em> can reason with and about equations. |
|
35 Linear <em>arithmetic</em> facts are proved automatically. Isabelle is |
|
36 closely integrated with the <a |
|
37 href="http://proofgeneral.inf.ed.ac.uk/">Proof |
|
38 General</a> user interface, which eases the task of writing and |
|
39 maintaining proof scripts. </p> |
|
40 |
|
41 A hyperlinked <a href="PG-preview.mov">preview</a> demonstrating Isabelle and Proof |
|
42 General is provided in |
|
43 <a href="http://www.apple.com/quicktime/download/">QuickTime format</a>, |
|
44 and also as a non-hyperlinked <a href="PG-preview.pdf">PDF file</a>. |
|
45 |
|
46 <p>Isabelle comes with large theories of formally verified |
|
47 mathematics, including elementary number theory (for example, Gauss's |
|
48 law of quadratic reciprocity), analysis (basic properties of limits, |
|
49 derivatives and integrals), algebra (up to Sylow's theorem) and set |
|
50 theory (the relative consistency of the Axiom of Choice). Also |
|
51 provided are numerous examples arising from research into formal |
|
52 verification. Isabelle is <a href="dist/">distributed</a> free of |
|
53 charge to academic users.</p> |
|
54 |
|
55 <p>Ample <a href="dist/docs.html">documentation</a> is available, |
|
56 including a <a |
|
57 href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published |
|
58 by Springer-Verlag. Several <a |
|
59 href="http://www.cl.cam.ac.uk/users/lcp/papers/isabelle.html">papers</a> |
|
60 on the design of Isabelle are available. There is also a list of past |
|
61 and present <a |
|
62 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a> |
|
63 undertaken using Isabelle. </p> |
|
64 |
|
65 <p>Isabelle is a joint project between <a |
|
66 href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</a> |
|
67 (University of Cambridge, UK) and <a |
|
68 href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a> (Technical |
|
69 University of Munich, Germany).</p> |
|