A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL

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

A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL

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

Department of Applied Mathematics and Computer Science

Aalborg University

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

161 Downloads (Orbit)

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 (AFP). 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 constitutes a framework for mechanically-checked completeness proofs for a range of proof systems.

Original language	English
Title of host publication	Proceedings of the 36^th Italian Conference on Computational Logic
Publisher	CEUR-WS
Publication date	2021
Pages	107-121
Publication status	Published - 2021
Event	36^th Italian Conference on Computational Logic - Centro Sant’Elisabetta, Parma, Italy Duration: 7 Sept 2021 → 9 Sept 2021 http://www.ailab.unipr.it/cilc21/

Conference

Conference	36^th Italian Conference on Computational Logic
Location	Centro Sant’Elisabetta
Country/Territory	Italy
City	Parma
Period	07/09/2021 → 09/09/2021
Internet address	http://www.ailab.unipr.it/cilc21/

Series	CEUR Workshop Proceedings
Volume	3002
ISSN	1613-0073

Access to Document

FulltextFinal published version, 536 KB

OpenUrl availability

Full text

Cite this

@inproceedings{a04249b1546340a4a229c8fbb27c1e16,

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 “First-Order Logic According to Fitting” by Berghofer in the Archive of Formal Proofs (AFP). 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 constitutes a framework for mechanically-checked completeness proofs for a range of proof systems. ",

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

year = "2021",

language = "English",

series = "CEUR Workshop Proceedings",

publisher = "CEUR-WS",

pages = "107--121",

booktitle = "Proceedings of the 36th Italian Conference on Computational Logic",

note = "36<sup>th</sup> Italian Conference on Computational Logic, CILC 2021 ; Conference date: 07-09-2021 Through 09-09-2021",

url = "http://www.ailab.unipr.it/cilc21/",

}

A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL. / From, Asta Halkjær; Schlichtkrull, Anders; Villadsen, Jørgen.
Proceedings of the 36^th Italian Conference on Computational Logic. CEUR-WS, 2021. p. 107-121 (CEUR Workshop Proceedings, Vol. 3002).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL

AU - From, Asta Halkjær

AU - Schlichtkrull, Anders

AU - Villadsen, Jørgen

PY - 2021

Y1 - 2021

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 (AFP). 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 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 (AFP). 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 constitutes a framework for mechanically-checked completeness proofs for a range of proof systems.

M3 - Article in proceedings

T3 - CEUR Workshop Proceedings

SP - 107

EP - 121

BT - Proceedings of the 36th Italian Conference on Computational Logic

PB - CEUR-WS

T2 - 36<sup>th</sup> Italian Conference on Computational Logic

Y2 - 7 September 2021 through 9 September 2021

ER -

A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this