Isabelle-92 ==>
Isabelle
<theory, tool> A generic theorem prover with support for several
object-logics, developed by Lawrence C. Paulson
<Larry.Paulson@cl.cam.ac.uk> in collaboration with Tobias 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.
Home.
Mailing list: isabelle-users@cl.cam.ac.uk.
["tactics"? "tacticals"?]
(1999-07-26)
Nearby terms:
IS-11172 « IS-13818 « ISA « Isabelle »
Isabelle-92 » Isabelle-93 » ISA bus
|