Talks and Poster Presentations (with Proceedings-Entry):
B. Kiesl, M. Suda, M. Seidl, H. Tompits, A. Biere:
"Blocked Clauses in First-Order Logic";
Talk: Lpar-21: 21st International Conference On Logic For Programming, Artificial Intelligence And Reasoning,
- 2017-05-12; in: "LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning",
EasyChair EPiC Series in Computing,
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.
automated theorem proving, first-order logic, preprocessing, sat, automated reasoning, clause elimination, blocked clauses
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.