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

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

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

142 Downloads (Pure)

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 languageEnglish
Title of host publicationProceedings of the 36th Italian Conference on Computational Logic
PublisherCEUR-WS
Publication date2021
Pages107-121
Publication statusPublished - 2021
Event36th Italian Conference on Computational Logic - Centro Sant’Elisabetta, Parma, Italy
Duration: 7 Sept 20219 Sept 2021
http://www.ailab.unipr.it/cilc21/

Conference

Conference36th Italian Conference on Computational Logic
LocationCentro Sant’Elisabetta
Country/TerritoryItaly
CityParma
Period07/09/202109/09/2021
Internet address
SeriesCEUR Workshop Proceedings
Volume3002
ISSN1613-0073

Fingerprint

Dive into the research topics of 'A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this