<div class="csl-bib-body">
<div class="csl-entry">Kiesl, B., Suda, M., Seidl, M., Tompits, H., & Biere, A. (2017). Blocked Clauses in First-Order Logic. In <i>LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i>. EasyChair. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3121</div>
</div>
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.
en
dc.description.sponsorship
Austrian Science Funds (FWF)
-
dc.description.sponsorship
ERC Starting Grant 2014 SYMCAR
-
dc.language
English
-
dc.language.iso
en
-
dc.publisher
EasyChair
-
dc.relation.ispartofseries
EPiC Series in Computing
-
dc.subject
first-order logic
en
dc.subject
automated reasoning
en
dc.subject
automated theorem proving
en
dc.subject
preprocessing
en
dc.subject
blocked clauses
en
dc.subject
clause elimination
en
dc.title
Blocked Clauses in First-Order Logic
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.relation.publication
LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
-
dc.relation.grantno
W1255-N23
-
dc.relation.grantno
S11403-N23
-
dc.relation.grantno
S11408-N23
-
dc.relation.grantno
S11409-N23
-
dc.relation.grantno
639270
-
dc.rights.holder
The Author(s)
-
dc.type.category
Full-Paper Contribution
-
tuw.container.volume
46
-
tuw.version
am
-
tuw.publication.orgunit
E192 - Institut für Informationssysteme
-
dc.identifier.libraryid
AC11363054
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:3-3121
-
tuw.author.orcid
0000-0003-3522-3653
-
tuw.author.orcid
0000-0002-3267-4494
-
tuw.author.orcid
0000-0001-5673-2460
-
tuw.author.orcid
0000-0001-7170-9242
-
item.openairetype
conference paper
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
item.languageiso639-1
en
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
item.grantfulltext
open
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E188 - Institut für Softwaretechnik und Interaktive Systeme
-
crisitem.author.dept
E192-03 - Forschungsbereich Knowledge Based Systems