Isabelle's Metalogic: Formalization and Proof Checker

Tobias Nipkow and Simon Roßkopf

Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.

arXiv

BibTeX:

@inproceedings{NipkowRosskopf-CADE21,author={Tobias Nipkow and Simon Ro{\ss}kopf},
title={Isabelle's Metalogic: Formalization and Proof Checker},
booktitle="Automated Deduction --- CADE-28",editor={A. Platzer and G. Sutcliff},
year=2021,publisher={Springer},series={LNCS},volume={12699},pages={93--110}}
Springer's final version

Isabelle formalization