Isabelle

theory, tool A generic theorem prover with support for

several object-logics, developed by Lawrence C. Paulson

[email protected] 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

HOL; Zermelo Frankel set theory; an extensional version

of Martin Lof'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: [email protected].

["tactics"? "tacticals"?]

(1999-07-26)