The foundation of a generic theorem prover

Isabelle 28, 30] is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or logical framework) in which the object-logics are formalized. Isabelle is now based on higher-order logic-a precise and well-understood foundation.Examples illustrate the use of this meta-logic to formalize logics and proofs. Axioms for first-order logic are shown to be sound and complete. Backwards proof is formalized by meta-reasoning about object-level entailment.Higher-order logic has several practical advantages over other meta-logics. Many proof techniques are known, such as Huet's higher-order unification procedure.