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 条
  • [41] Liveness Reasoning with Isabelle/HOL
    Wang, Jinshuang
    Yang, Huabing
    Zhang, Xingyuan
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2009, 5674 : 485 - 499
  • [42] Formalization of Euler-Lagrange Equation Set Based on Variational Calculus in HOL Light
    Guan, Yong
    Zhang, Jingzhi
    Wang, Guohui
    Li, Ximeng
    Shi, Zhiping
    Li, Yongdong
    JOURNAL OF AUTOMATED REASONING, 2021, 65 (01) : 1 - 29
  • [43] On the Formalization of Gamma Function in HOL
    Siddique, Umair
    Hasan, Osman
    JOURNAL OF AUTOMATED REASONING, 2014, 53 (04) : 407 - 429
  • [44] Comprehending Isabelle/HOL's Consistency
    Kuncar, Ondrej
    Popescu, Andrei
    PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2017): 26TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2017, 10201 : 724 - 749
  • [45] Fast Machine Words in Isabelle/HOL
    Lochbihler, Andreas
    INTERACTIVE THEOREM PROVING, ITP 2018, 2018, 10895 : 388 - 410
  • [46] On the Formalization of Gamma Function in HOL
    Umair Siddique
    Osman Hasan
    Journal of Automated Reasoning, 2014, 53 : 407 - 429
  • [47] A Denotational Semantics of Solidity in Isabelle/HOL
    Marmsoler, Diego
    Brucker, Achim D.
    SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2021), 2021, 13085 : 403 - 422
  • [48] Automating Free Logic in Isabelle/HOL
    Benzmueller, Christoph
    Scott, Dana
    MATHEMATICAL SOFTWARE, ICMS 2016, 2016, 9725 : 43 - 50
  • [49] Verified Real Asymptotics in Isabelle/HOL
    Eberl, Manuel
    PROCEEDINGS OF THE 2019 ACM INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC '19), 2019, : 147 - 154
  • [50] Extracting a normalization algorithm in Isabelle/HOL
    Berghofer, S
    TYPES FOR PROOFS AND PROGRAMS, 2006, 3839 : 50 - 65
12345