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

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

Research output: Contribution to journalJournal articleResearchpeer-review

1 Citation (Scopus)

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 languageEnglish
JournalJournal of Logic and Computation
Volume33
Issue number4
Pages (from-to)818-836
Number of pages19
ISSN0955-792X
DOIs
Publication statusPublished - 1 Jun 2023

Keywords

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

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