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 36th Italian Conference on Computational Logic |
Publisher | CEUR-WS |
Publication date | 2021 |
Pages | 107-121 |
Publication status | Published - 2021 |
Event | 36th 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 | 36th Italian Conference on Computational Logic |
---|---|
Location | Centro Sant’Elisabetta |
Country/Territory | Italy |
City | Parma |
Period | 07/09/2021 → 09/09/2021 |
Internet address |
Series | CEUR Workshop Proceedings |
---|---|
Volume | 3002 |
ISSN | 1613-0073 |