Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses

被引：7
作者：
Gorzny, Jan [1 ]
Paleo, Bruno Woltzenlogel [2 ]
机构：
[1] Univ Victoria, Victoria, BC, Canada
[2] Vienna Univ Technol, A-1040 Vienna, Austria
来源：
AUTOMATED DEDUCTION - CADE-25 | 2015年 / 9195卷
关键词：
D O I：
10.1007/978-3-319-21401-6_24
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
The recently developed LowerUnits algorithm compresses propositional resolution proofs generated by SAT- and SMT-solvers by postponing and lowering resolution inferences involving unit clauses, which have exactly one literal. This paper describes a generalization of this algorithm to the case of first-order resolution proofs generated by automated theorem provers. An empirical evaluation of a simplified version of this algorithm on hundreds of proofs shows promising results.
引用
收藏
页码：356 / 366
页数：11
相关论文
共 12 条
  • [1] Bar-Ilan O, 2009, LECT NOTES COMPUT SC, V5394, P114
  • [2] Boudou J., 2013, TABLEAUX 2013 LNCS, V8123, P59
  • [3] Boudou J, 2014, LECT NOTES ARTIF INT, V8562, P374, DOI 10.1007/978-3-319-08587-6_29
  • [4] Fontaine P., 2010, 8 INT WORKSH SMT ED
  • [5] Fontaine P, 2011, LECT NOTES ARTIF INT, V6803, P237, DOI 10.1007/978-3-642-22438-6_19
  • [6] Hetzl S, 2008, LECT NOTES ARTIF INT, V5144, P462, DOI 10.1007/978-3-540-85110-3_38
  • [7] Algorithmic introduction of quantified cuts
    Hetzl, Stefan
    Leitsch, Alexander
    Reis, Giselle
    Weller, Daniel
    [J]. THEORETICAL COMPUTER SCIENCE, 2014, 549 : 1 - 16
  • [8] Paleo BW, 2010, LECT NOTES ARTIF INT, V6355, P463, DOI 10.1007/978-3-642-17511-4_26
  • [9] Rollini S.F., 2010, HVC 2010 LNCS, V6504, P182
  • [10] The TPTP Problem Library and Associated Infrastructure
    Sutcliffe, Geoff
    [J]. JOURNAL OF AUTOMATED REASONING, 2009, 43 (04) : 337 - 362
12