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

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

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

1 Citationer (Scopus)


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.
TidsskriftJournal of Logic and Computation
Udgave nummer4
Sider (fra-til)818-836
Antal sider19
StatusUdgivet - 1 jun. 2023

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


Dyk ned i forskningsemnerne om 'A sequent calculus for first-order logic formalized in Isabelle/HOL.'. Sammen danner de et unikt fingeraftryk.