What is Isabelle?
-- Isabelle is a generic proof assistant. It allows mathematical - formulas to be expressed in a formal language and provides tools - for proving those formulas in a logical calculus. The main - application is the formalization of mathematical proofs and in - particular formal verification, which includes proving - the correctness of computer hardware or software and proving - properties of computer languages and protocols.
- -Compared with similar tools, Isabelle's distinguishing feature is its - flexibility. Most proof assistants are built around a single formal calculus, - typically higher-order logic. Isabelle has the capacity to accept a variety - of formal calculi. The distributed version supports higher-order logic but - also axiomatic set theory and several other formalisms. See - logics for more details.
- -Isabelle is a joint project between Lawrence C. Paulson - (University of Cambridge, UK) and Tobias Nipkow (Technical - University of Munich, Germany).
- -Isabelle is distributed freely as Open Source - Software BSD - license; see the installation instructions.
- -Preview of Isabelle
- - -
-
-
- Here is a hyperlinked preview demonstrating - Isabelle and ProofGeneral, in QuickTime - format and in PDF.
-- -
What Isabelle offers
- -Isabelle provides excellent notational support: new notations - can be introduced, using normal mathematical symbols. Proofs can - be written in a structured notation based upon traditional proof - style, or more straightforwardly as sequences of - commands. Definitions and proofs may include TeX source, from - which Isabelle can automatically generate typeset documents.
- -The main limitation of all such proof systems is that proving - theorems requires much effort from an expert user. Isabelle - incorporates some tools to improve the user's productivity by - automating some parts of the proof process. In particular, - Isabelle's classical reasoner can perform long chains - of reasoning steps to prove formulas. The simplifier - can reason with and about equations. Linear arithmetic - facts are proved automatically.
- -Isabelle comes with a large theory library of formally - verified mathematics, including elementary number theory (for - example, Gauss's law of quadratic reciprocity), analysis (basic - properties of limits, derivatives and integrals), algebra (up to - Sylow's theorem) and set theory (the relative consistency of the - Axiom of Choice). Also provided are numerous examples arising - from research into formal verification.
- -With Isar, Isabelle offers a concise proof formulation language - which enables a user to write proof scripts naturally understandable for - both humans and computers.
- -Isabelle is closely integrated with the ProofGeneral user interface, which - eases the task of writing and maintaining proof scripts.
- -Ample documentation is available - about using Isabelle and its inner concepts, including a - Tutorial published by - Springer-Verlag.
- -