Isabelle is a popular generic theorem prover developed at Cambridge University and TU Munich. Existing logics like Isabelle/HOL provide a theorem proving environment ready to use for sizable applications. Isabelle may also serve as framework for rapid prototyping of deductive systems. It comes with a large library including Isabelle/HOL (classical higher-order logic), Isabelle/HOLCF (Scott's Logic for Computable Functions with HOL), Isabelle/FOL (classical and intuitionistic first-order logic), and Isabelle/ZF (Zermelo-Fraenkel set theory on top of FOL).
|Tags||education Scientific/Engineering Mathematics|
|Operating Systems||POSIX Linux Mac OS X Solaris|
Release Notes: This release contains major enhancements in specification elements, the user interface, and proof tools. The most notable additions on the theorem proving and specification side are 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, this release contains a new, general find-theorems command (by term patterns, as intro/elim/simp rules etc.), new commands for generating adhoc draft documents, and support for Unicode proof documents.
Release Notes: The library of the HOL4 system (about 2,500 additional theorems) has been imported. Theories for rational numbers, rings, and matrices have been added, as well as over 250 basic numerical laws for semirings, rings, and fields. Handling of linear and partial orders has been improved. Two commands to search for counterexamples have been added. Presentation and x-symbol handling has been improved.
Release Notes: This release has a new framework for extracting programs from constructive proofs in HOL, full Presburger arithmetic, locales (named proof contexts), and an improved simplifier. Library additions include HOL/Algebra (proofs in classical algebra), HOL/Complex (complex numbers with numeric constants and some complex analysis, including nonstandard analysis), HOL/NumberTheory (Gauss's law of quadratic reciprocity), and ZF/Constructible (Gödel's proof of the relative consistency of the axiom of choice).
Release Notes: The Isabelle/HOL tutorial is to be published as book (LNCS volume 2283). Isabelle now supports explicit proof terms, a better locale package, and an ML code generator for functional and relational specifications. The document preparation tools have been simplified. Poly/ML 4.1.1 and 4.1.2 are supported. MacOS X support has been improved. Library additions include: Bali (formal treatment of Java), HoareParallel (verification of parallel imperative programs), group theory examples including Sylow's theorem, and a typeless version of Chandy and Misra's formalism (ZF/UNITY).
Release Notes: This release includes several improvements to document preparation (antiquotations, improved style files, and sub/super scripts), improvements to the Isar proof language (better obtain, better induct, and a conversion script for legacy ML files), improvements to HOL (small structural changes, better arithmetic for reals), improvements to the simplifier (implemented a derived rule), and support for Poly/ML 4.0.