The foundation of a generic theorem prover

The logical framework of the interactive theorem prover ISABELLE is laid down. ISABELLE is constructed to support a variety of logics: Martin- Löf's type theory, Zermelo-Fraenkel set theory, intuitionistic and classical sequent calculi. It is implemented in Standard ML. To meet the needs of a generic theorem prover like ISABELLE a higher- order logic or meta-logic is established to build proofs in those various object-logics. On the meta-level ISABELLE incorporates intuitionistic higher-order logic to ease proofs by deductions, i.e. rules are represented as propositions and combined to yield proofs. Natural deduction, object-level backwards proofs with examples from propositional and first order logic both of them in classical as well as intuitionistic form are highlighted as practical applications of ISABELLE. Theoretical issues like sound- and completeness are shown to remain valid. Advantages over LCF, AUTOMATH and an earlier version of ISABELLE - ISABELLE-86 - are considered with respect to computational complexity of proof constructions.

Recommendations

Cites work

Cited in

(99)

Describes a project that uses

Uses Software

This page was built for publication: The foundation of a generic theorem prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1823013)