|
About:
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).
Release focus: Major feature enhancements
Changes:
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.
Author:
The Isabelle Team <isabelle (dash) enquiries (at) cl (dot) cam (dot) ac (dot) uk>
[contact developer]
Homepage:
http://isabelle.in.tum.de/
Changelog:
http://isabelle.in.tum.de/dist/Isabelle/NEWS
Mirror site:
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
Trove categories:
[change]
Dependencies:
[change]
Proof General (Default branch) (recommended)
[download links]
|
|
» Rating:
8.40/10.00
(Rank N/A)
» Vitality: 0.00% (Rank 7321)
» Popularity: 0.70% (Rank 8592)
 
(click to enlarge graphs)
Record hits: 8,119
URL hits: 2,711
Subscribers: 16
|
|
