Zur Seitenansicht


Blocked Clauses in First-Order Logic
VerfasserKiesl, Benjamin ; Suda, Martin In der Gemeinsamen Normdatei der DNB nachschlagen ; Seidl, Martina In der Gemeinsamen Normdatei der DNB nachschlagen ; Tompits, Hans ; Biere, Armin In der Gemeinsamen Normdatei der DNB nachschlagen
Erschienen in
LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017, S. 31-48
ErschienenEasyChair, 2017
Accepted version
SerieEPiC Series in Computing ; 46
DokumenttypAufsatz in einem Sammelwerk
Schlagwörter (EN)first-order logic / automated reasoning / automated theorem proving / preprocessing / blocked clauses / clause elimination
Projekt-/ReportnummerAustrian Science Fund (FWF): W1255-N23
Projekt-/ReportnummerAustrian Science Fund (FWF): S11403-N23
Projekt-/ReportnummerAustrian Science Fund (FWF): S11408-N23
Projekt-/ReportnummerAustrian Science Fund (FWF): S11409-N23
Projekt-/ReportnummerERC Starting Grant 2014 SYMCAR 639270
URNurn:nbn:at:at-ubtuw:3-3121 Persistent Identifier (URN)
 Das Werk ist frei verfügbar
Blocked Clauses in First-Order Logic [0.4 mb]
Zusammenfassung (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 whose elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.