Isabelle
Summary
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).
Authors
Isabelle is a joint project between Lawrence C. Paulson (University of Cambridge, UK) and Tobias Nipkow (Technical University of Munich, Germany).
Vendor
Isabelle is distributed freely as Open Source Software BSD license.
Links
Status
officially approved by the authors