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