A Formalization and Proof Checker for Isabelle’s Metalogic

Simon Roßkopf; Tobias Nipkow

doi:10.1007/s10817-022-09648-w

A Formalization and Proof Checker for Isabelle’s Metalogic

Simon Roßkopf, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Article number	1
Journal	Journal of Automated Reasoning
Volume	67
Issue number	1
DOIs	https://doi.org/10.1007/s10817-022-09648-w
State	Published - Mar 2023

Keywords

Higher-order logic
Isabelle
Metalogic
Proofchecker
Theorem proving

Access to Document

10.1007/s10817-022-09648-w

Cite this

@article{e3773efb35e547c7a7a25bdf267c85b3,

title = "A Formalization and Proof Checker for Isabelle{\textquoteright}s Metalogic",

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.",

keywords = "Higher-order logic, Isabelle, Metalogic, Proofchecker, Theorem proving",

author = "Simon Ro{\ss}kopf and Tobias Nipkow",

note = "Publisher Copyright: {\textcopyright} 2022, The Author(s).",

year = "2023",

month = mar,

doi = "10.1007/s10817-022-09648-w",

language = "English",

volume = "67",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "1",

}

TY - JOUR

T1 - A Formalization and Proof Checker for Isabelle’s Metalogic

AU - Roßkopf, Simon

AU - Nipkow, Tobias

PY - 2023/3

Y1 - 2023/3

N2 - 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.

AB - 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.

KW - Higher-order logic

KW - Isabelle

KW - Metalogic

KW - Proofchecker

KW - Theorem proving

UR - http://www.scopus.com/inward/record.url?scp=85143722709&partnerID=8YFLogxK

U2 - 10.1007/s10817-022-09648-w

DO - 10.1007/s10817-022-09648-w

M3 - Article

AN - SCOPUS:85143722709

SN - 0168-7433

VL - 67

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 1

M1 - 1

ER -

A Formalization and Proof Checker for Isabelle’s Metalogic

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this