Isabelle
Isabelle-92
Isabelle-93
<theory, tool> A generic {theorem prover} with support for
several {object-logics}, developed by Lawrence C. Paulson
<[email protected]> in collaboration with Tobias
Nipkow (http://in.tum.de/~nipkow/) at the Technical
University of Munich.
A system of {type classes} allows {polymorphic} object-logics
with {overloading} and automatic {type inference}.
Isabelle supports {first-order logic} - {constructive} and
classical versions; {higher-order logic}, similar to Gordon's
{HOL}; {Zermelo Fränkel set theory}; an {extensional} version
of {Martin Löf}'s {type theory}, the classical first-order
{sequent calculus}, {LK}; the {modal logics} {T}, {S4}, and
{S43}; and {Logic for Computable Functions}.
An object logic's {syntax} and {inference rules} are specified
{declaratively} allowing single-step proof construction.
{Proof procedures} can be expressed using "tactics" and
"tacticals". Isabelle provides control structures for
expressing search procedures and generic tools such as
simplifiers and classical theorem provers which can be applied
to object-logics. Isabelle is built on top of {Standard ML}
and uses its user interface.
(http://cl.cam.ac.uk/Research/HVG/Isabelle/).
Mailing list: [email protected].
["tactics"? "tacticals"?]
(1999-07-26)