A Formalization and Proof Checker for Isabelle’s Metalogic

Autor:	Simon Roßkopf, Tobias Nipkow
Rok vydání:	2022
Předmět:	Computational Theory and Mathematics Artificial Intelligence Software
Zdroj:	Journal of Automated Reasoning. 67
ISSN:	1573-0670 0168-7433
DOI:	10.1007/s10817-022-09648-w
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::95982e8f385bce8a6644ab9ed796b5e4 https://doi.org/10.1007/s10817-022-09648-w Zobrazit plný text záznamu Full text from SpringerLink