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

被引：1
|
作者：
From, Asta Halkjaer [1 ]
Schlichtkrull, Anders [2 ]
Villadsen, Jorgen [1 ]
机构：
[1] Tech Univ Denmark, Lyngby, Denmark
[2] Aalborg Univ, Copenhagen, Denmark
来源：
JOURNAL OF LOGIC AND COMPUTATION | 2023年 / 33卷 / 04期
关键词：
sequent calculus; tableau calculus; first-order logic; soundness; completeness; Isabelle; HOL;
D O I：
10.1093/logcom/exad013
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：818 / 836
页数：19
相关论文
共 50 条
  • [1] Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
    From, Asta Halkjaer
    Jacobsen, Frederik Krogsdal
    [J]. JOURNAL OF AUTOMATED REASONING, 2024, 68 (03)
  • [2] A Sequent Calculus for First-Order Logic
    Braselmann, Patrick
    Koepke, Peter
    [J]. FORMALIZED MATHEMATICS, 2005, 13 (01): : 33 - 39
  • [3] SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
    From, Asta Halkjaer
    Jacobsen, Frederik Krogsdal
    Villadsen, Jorgen
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (357): : 38 - 55
  • [4] SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
    From, Asta Halkjær
    Jacobsen, Frederik Krogsdal
    Villadsen, Jørgen
    [J]. Electronic Proceedings in Theoretical Computer Science, EPTCS, 2022, 357 : 38 - 55
  • [5] A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
    Rummer, Philipp
    [J]. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, 2008, 5330 : 274 - 289
  • [6] Using Isabelle/HOL to Verify First-Order Relativity Theory
    Mike Stannett
    István Németi
    [J]. Journal of Automated Reasoning, 2014, 52 : 361 - 378
  • [7] Using Isabelle/HOL to Verify First-Order Relativity Theory
    Stannett, Mike
    Nemeti, Istvan
    [J]. JOURNAL OF AUTOMATED REASONING, 2014, 52 (04) : 361 - 378
  • [8] Programming and verifying a declarative first-order prover in Isabelle/HOL
    Jensen, Alexander Birch
    Larsen, John Bruntse
    Schlichtkrull, Anders
    Villadsen, Jorgen
    [J]. AI COMMUNICATIONS, 2018, 31 (03) : 281 - 299
  • [9] Non-Commutative First-Order Sequent Calculus
    Tatsuta, Makoto
    [J]. COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2009, 5771 : 470 - 484
  • [10] Lyndon Words Formalized in Isabelle/HOL
    Holub, Stepan
    Starosta, Stepan
    [J]. DEVELOPMENTS IN LANGUAGE THEORY, DLT 2021, 2021, 12811 : 217 - 228
12345