Isabelle's Metalogic: Formalization and Proof Checker
Logic in Computer Science
2021-11-25 v1
Abstract
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.
Cite
@article{arxiv.2104.12224,
title = {Isabelle's Metalogic: Formalization and Proof Checker},
author = {Tobias Nipkow and Simon Roßkopf},
journal= {arXiv preprint arXiv:2104.12224},
year = {2021}
}
Comments
to be published in In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28), LNCS, Springer, 2021