The Foundation of a Generic Theorem Prover
<|reference_start|>The Foundation of a Generic Theorem Prover: Isabelle 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 use of this meta-logic to formalize logics and proofs. Axioms for first-order logic are shown 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.<|reference_end|>
@article{paulson2000the,
    title={The Foundation of a Generic Theorem Prover},
    author={Lawrence C. Paulson},
    journal={Journal of Automated Reasoning 5 (1989), 363-397},
    year={2000},
    archivePrefix={arXiv},
    eprint={cs/9301105},
    primaryClass={cs.LO}
}