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), Technische Universität München (Tobias Nipkow) and Université Paris-Sud (Makarius Wenzel). See the Isabelle overview for a brief introduction.
Now available: Isabelle2011-1
Notable changes:
- Significantly improved Isabelle/jEdit Prover IDE (PIDE).
- Improved system integration with Isabelle/Scala: YXML data encoding.
- Improved parallel performance and scalability.
- Improved document preparation: embedded rail-road diagrams.
- HOL tool enhancements: Quickcheck, Nitpick, Sledgehammer, SMT/Z3 integration.
- Numerous HOL library improvements: main HOL, HOLCF, HOL-Library, Multivariate_Analysis, Probability.
- Updated and extended Isabelle/Isar reference manual.
See also the cumulative NEWS.
Download & Support
Isabelle is distributed for free under the BSD license. It includes source and binary packages and 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.