The foundation of a generic theorem prover (Q1823013): Difference between revisions

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.