-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. 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 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 is -closely integrated with the Proof -General user interface, which eases the task of writing and -maintaining proof scripts.
- -A hyperlinked preview demonstrating Isabelle and Proof -General is provided in -QuickTime format, -and also as a non-hyperlinked PDF file. - -Isabelle comes with large theories 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. Isabelle is distributed free of -charge to academic users.
- -Ample documentation is available, -including a Tutorial published -by Springer-Verlag. Several papers -on the design of Isabelle are available. There is also a list of past -and present projects -undertaken using Isabelle.
- -Isabelle is a joint project between Lawrence C. Paulson -(University of Cambridge, UK) and Tobias Nipkow (Technical -University of Munich, Germany).