SAT-Based Subsumption Resolution

被引：1

作者：

Coutelier, Robin ^{[1
]}

Kovacs, Laura ^{[2
]}

Rawson, Michael ^{[2
]}

Rath, Jakob ^{[2
]}

机构：

[1] Univ Liege, Liege, Belgium

[2] TU Wien, Vienna, Austria

来源：

AUTOMATED DEDUCTION, CADE 29 | 2023年 / 14132卷

关键词：

D O I：

10.1007/978-3-031-38499-8_11

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlying saturation algorithm. We implemented our work in the theorem prover VAMPIRE, and show that it is noticeably faster than the state of the art.

引用

页码：190 / 206

页数：17

共 18 条

[1]

Bachmair L., 1994, Journal of Logic and Computation, V4, P217, DOI 10.1093/logcom/4.3.217

[2]

Bachmair L., 2001, HDB AUTOMATED REASON, P19

[3] Subsumption Demodulation in First-Order Theorem Proving [J].

Gleiss, Bernhard ;

Kovacs, Laura ;

Rath, Jakob .

AUTOMATED REASONING, PT I, 2020, 12166 :297-315

[4]

KAPUR D, 1986, LECT NOTES COMPUT SC, V230, P489

[5]

Korovin Konstantin, 2013, Programming Logics. Essays in Memory of Harald Ganzinger: LNCS 7797, P239, DOI 10.1007/978-3-642-37651-1_10

[6]

Kovacs Laura, 2013, Computer Aided Verification. 25th International Conference, CAV 2013. Proceedings. LNCS 8044, P1, DOI 10.1007/978-3-642-39799-8_1

[7] Otter - The CADE-13 competition incarnations [J].

McCune, W ;

Wos, L .

JOURNAL OF AUTOMATED REASONING, 1997, 18 (02) :211-220

[8]

Nieuwenhuis R., 2001, HDB AUTOMATED REASON, VI, P371, DOI DOI 10.1016/B978-044450813-3/50009-6

[9]

Ramakrishnan I. V., 2001, HDB AUTOMATED REASON, VII, P1853

[10] First-Order Subsumption via SAT Solving [J].

Rath, Jakob ;

Biere, Armin ;

Kovacs, Laura .

2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD, 2022, 3 :160-169

← 1 2 →