A sequent calculus for first-order logic formalized in Isabelle/HOL.

Asta Halkjær From; Anders Schlichtkrull; Jørgen Villadsen

doi:10.1093/LOGCOM/EXAD013

A sequent calculus for first-order logic formalized in Isabelle/HOL.

Asta Halkjær From, Anders Schlichtkrull, Jørgen Villadsen

Research output: Contribution to journal › Journal article › Research › peer-review

Abstract

We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry ‘First-Order Logic According to Fitting’ by Berghofer in the Archive of Formal Proofs. The calculi and proof techniques are taken from Ben-Ari’s textbook Mathematical Logic for Computer Science (Springer, 2012). We thereby demonstrate that Berghofer’s approach works not only for natural deduction but also constitutes a framework for mechanically checked completeness proofs for a range of proof systems.

Original language	English
Journal	Journal of Logic and Computation
Volume	33
Issue number	4
Pages (from-to)	818-836
Number of pages	19
ISSN	0955-792X
DOIs	https://doi.org/10.1093/LOGCOM/EXAD013
Publication status	Published - 1 Jun 2023

Keywords

Isabelle/HOL
completeness
first-order logic
sequent calculus
soundness
tableau calculus

Access to Document

10.1093/LOGCOM/EXAD013

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@article{31f86a083f4f49d2a646e951d3b4534e,

title = "A sequent calculus for first-order logic formalized in Isabelle/HOL.",

abstract = "We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry {\textquoteleft}First-Order Logic According to Fitting{\textquoteright} by Berghofer in the Archive of Formal Proofs. The calculi and proof techniques are taken from Ben-Ari{\textquoteright}s textbook Mathematical Logic for Computer Science (Springer, 2012). We thereby demonstrate that Berghofer{\textquoteright}s approach works not only for natural deduction but also constitutes a framework for mechanically checked completeness proofs for a range of proof systems.",

keywords = "Isabelle/HOL, completeness, first-order logic, sequent calculus, soundness, tableau calculus",

author = "From, {Asta Halkj{\ae}r} and Anders Schlichtkrull and J{\o}rgen Villadsen",

note = "DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.",

year = "2023",

month = jun,

day = "1",

doi = "10.1093/LOGCOM/EXAD013",

language = "English",

volume = "33",

pages = "818--836",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

publisher = "Oxford University Press",

number = "4",

}

TY - JOUR

T1 - A sequent calculus for first-order logic formalized in Isabelle/HOL.

AU - From, Asta Halkjær

AU - Schlichtkrull, Anders

AU - Villadsen, Jørgen

N1 - DBLP's bibliographic metadata records provided through http://dblp.org/search/publ/api are distributed under a Creative Commons CC0 1.0 Universal Public Domain Dedication. Although the bibliographic metadata records are provided consistent with CC0 1.0 Dedication, the content described by the metadata records is not. Content may be subject to copyright, rights of privacy, rights of publicity and other restrictions.

PY - 2023/6/1

Y1 - 2023/6/1

N2 - We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry ‘First-Order Logic According to Fitting’ by Berghofer in the Archive of Formal Proofs. The calculi and proof techniques are taken from Ben-Ari’s textbook Mathematical Logic for Computer Science (Springer, 2012). We thereby demonstrate that Berghofer’s approach works not only for natural deduction but also constitutes a framework for mechanically checked completeness proofs for a range of proof systems.

AB - We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry ‘First-Order Logic According to Fitting’ by Berghofer in the Archive of Formal Proofs. The calculi and proof techniques are taken from Ben-Ari’s textbook Mathematical Logic for Computer Science (Springer, 2012). We thereby demonstrate that Berghofer’s approach works not only for natural deduction but also constitutes a framework for mechanically checked completeness proofs for a range of proof systems.

KW - Isabelle/HOL

KW - completeness

KW - first-order logic

KW - sequent calculus

KW - soundness

KW - tableau calculus

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

U2 - 10.1093/LOGCOM/EXAD013

DO - 10.1093/LOGCOM/EXAD013

M3 - Journal article

SN - 0955-792X

VL - 33

SP - 818

EP - 836

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 4

ER -

A sequent calculus for first-order logic formalized in Isabelle/HOL.

Abstract

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

Cite this