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. Isabelle is developed at University of Cambridge (Larry Paulson) and Technische Universität München (Tobias Nipkow). See the Isabelle overview for a brief introduction.
Now available: Isabelle2009-1
Important changes:
- Isabelle tool wwwfind provides web interface for find_theorems on a given logic image.
- HOL-SMT: proof method smt for a combination of first-order logic with equality, linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors.
- HOL-Boogie: an interactive prover back-end for Boogie and VCC.
- HOL: counterexample generator tool Nitpick based on the Kodkod relational model finder.
- HOL: predicate compiler turning inductive into (executable) equational specifications.
- HOL: refined number theory.
- HOL: various parts of multivariate analysis.
- HOL-Library: proof method sos (sum of squares) for nonlinear real arithmetic, based on external semidefinite programming solvers.
- HOLCF: new definitional domain package.
- Revised tutorial on locales.
- ML: tacticals for subgoal focus.
- ML: support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.
- Parallel checking of nested Isar proofs, with improved scalability up to 8 cores.
See also the cumulative NEWS.
Download & Support
Isabelle is distributed for free under the BSD license. It includes source and binary packages and browsable documentation, see the installation instructions.
A vast collection of Isabelle examples and applications is available from the Archive of Formal Proofs.
Support is available by ample documentation and the Isabelle community.