Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
B. Kiesl, M. Suda, M. Seidl, H. Tompits, A. Biere:
"Blocked Clauses in First-Order Logic";
Vortrag: Lpar-21: 21st International Conference On Logic For Programming, Artificial Intelligence And Reasoning,
Maun, Botswana;
07.05.2017
- 12.05.2017; in: "LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning",
EasyChair EPiC Series in Computing,
Volume 46
(2017),
S. 31
- 48.
Kurzfassung englisch:
Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper, we lift the notion of blocked clauses to first-order logic. We introduce two types of blocked clauses, one for first-order logic with equality and the other for first-order logic without equality, and prove their redundancy. In addition, we give a polynomial algorithm for checking whether a clause is blocked. Based on our new notions of blocking, we implemented a novel first-order preprocessing tool. Our experiments showed that many first-order problems in the TPTP library contain a large number of blocked clauses. Moreover, we observed that their elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.
Schlagworte:
automated theorem proving, first-order logic, preprocessing, sat, automated reasoning, clause elimination, blocked clauses
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_264657.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.