Search in: Word
Vietnamese keyboard: Off
Virtual keyboard: Show
Computing (FOLDOC) dictionary
Isabelle
Jump to user comments
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 TobiasNipkow at the TechnicalUniversity 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
of Martin Lof's type theory, the classical first-order
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.