We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
A sequent calculus for first-order logic formalized in Isabelle/HOL.
- Authors
From, Asta Halkjær; Schlichtkrull, Anders; Villadsen, Jørgen
- 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.
- Subjects
FIRST-order logic; COMPUTER logic; MATHEMATICAL logic; CALCULUS; CALCULI
- Publication
Journal of Logic & Computation, 2023, Vol 33, Issue 4, p818
- ISSN
0955-792X
- Publication type
Article
- DOI
10.1093/logcom/exad013