An Isabelle/HOL Formalization of the SCL(FOL) Calculus

被引：1
|
作者：
Bromberger, Martin [1 ]
Desharnais, Martin [1 ,2 ]
Weidenbach, Christoph [1 ]
机构：
[1] Max Planck Inst Informat, Saarland Informat Campus, Saarbrucken, Germany
[2] Saarland Informat Campus, Grad Sch Comp Sci, Saarbrucken, Germany
来源：
AUTOMATED DEDUCTION, CADE 29 | 2023年 / 14132卷
关键词：
interactive theorem proving; automated theorem proving; first-order logic; CDCL; SCL; non-redundant clause learning;
D O I：
10.1007/978-3-031-38499-8_7
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present an Isabelle/HOL formalization of Simple Clause Learning for first-order logic without equality: SCL(FOL). The main results are formal proofs of soundness, non-redundancy of learned clauses, termination, and refutational completeness. Compared to the unformalized version, the formalized calculus is simpler and more general, some results such as non-redundancy are stronger and some results such as non-subsumption are new. We found one bug in a previously published version of the SCL Backtrack rule. Compared to related formalizations, we introduce a new technique for showing termination based on non-redundant clause learning.
引用
收藏
页码：116 / 133
页数：18
相关论文
共 50 条
  • [1] A Modular Formalization of Superposition in Isabelle/HOL
    Desharnais, Martin
    Toth, Balazs
    Waldmann, Uwe
    Blanchette, Jasmin
    Tourret, Sophie
    Leibniz International Proceedings in Informatics, LIPIcs, 309
  • [2] Formalization of Differential Privacy in Isabelle/HOL
    Sato, Tetsuya
    Minamide, Yasuhiko
    PROCEEDINGS OF THE 14TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2025, 2025, : 67 - 82
  • [3] SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
    From, Asta Halkjaer
    Jacobsen, Frederik Krogsdal
    Villadsen, Jorgen
    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
    Electronic Proceedings in Theoretical Computer Science, EPTCS, 2022, 357 : 38 - 55
  • [5] A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL
    Li, Yongjian
    Hung, William N. N.
    Song, Xiaoyu
    THEORETICAL COMPUTER SCIENCE, 2011, 412 (25) : 2746 - 2765
  • [6] Software Component Design with the B Method - A Formalization in Isabelle/HOL
    Deharbe, David
    Merz, Stephan
    FORMAL ASPECTS OF COMPONENT SOFTWARE, 2016, 9539 : 31 - 47
  • [7] A Formalization of the C99 Standard in HOL, Isabelle and Coq
    Krebbers, Robbert
    Wiedijk, Freek
    INTELLIGENT COMPUTER MATHEMATICS, MKM 2011, 2011, 6824 : 301 - 303
  • [8] An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR
    Haslbeck, Max W.
    Thiemann, Rene
    CPP '21: PROCEEDINGS OF THE 10TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2021, : 238 - 249
  • [9] Formalization of Dube's Degree Bounds for Grobner Bases in Isabelle/HOL
    Maletzky, Alexander
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2019, 2019, 11617 : 155 - 170
  • [10] Importing HOL into Isabelle/HOL
    Obua, Steven
    Skalberg, Sebastian
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 298 - 302
12345