Isabelle, a widely used proven theorem tool, was created by Cambridge University and TU Munich.
Compared to other tools that perform similar tasks, Isabelle stands out due to its unique feature of flexibility. Most proof assistants depend on a single formal calculus, which is typically higher-order logic. However, Isabelle is capable of accommodating several formal calculi, including axiomatic set theory, among others. Furthermore, its distributed version supports higher-order logic, offering versatility to users. Isabelle is a collaborative project between Lawrence C. Paulson from the University of Cambridge, UK, and Tobias Nipkow from the Technical University of Munich, Germany.
Isabelle comes equipped with various features that make it stand out as an excellent software for proof assistance. These features include the interpretation of locale expressions in theories, locales, and proof contexts. The software also comes with substantial library improvements, proof tools for transitivity reasoning, a general find_theorems command (by term patterns, as intro/elim/simp rules, etc.), commands for generating adhoc draft documents, support for Unicode proof documents (UTF-8), and major internal reorganizations and performance improvements.
To use Isabelle, users require a full Standard ML Compiler (e.g., Poly/ML 4.1.x, SML/NJ 110.x), the GNU bash shell (version 2.x), Perl (version 5.x), XEmacs (version 21.4.x) for the ProofGeneral interface, and a complete LaTeX installation (e.g., teTeX 1.0) for document preparation.
The latest release of Isabelle contains significant enhancements in specification elements, the user interface, and proof tools. The most notable additions include interpretation of locale expressions in theories, locales, and proof contexts, substantial library improvements, proof tools for transitivity reasoning, and performance improvements. On the user interface side, Isabelle now features a new, general find-theorems command (by term patterns, as intro/elim/simp rules), new commands for generating adhoc draft documents, and support for Unicode proof documents.
Version 2005: N/A