<div class="csl-bib-body">
<div class="csl-entry">Vukmirović, P., Blanchette, J., & Heule, M. (2021). SAT-Inspired Eliminations for Superposition. In <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021</i> (pp. 231–240). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_32</div>
</div>
Optimized SAT solvers not only preprocess the
clause set, they also transform it during solving as inprocessing.
Some preprocessing techniques have been generalized to firstorder
logic with equality. In this paper, we port inprocessing
techniques to work with superposition, a leading first-order proof
calculus, and we strengthen known preprocessing techniques.
Specifically, we look into elimination of hidden literals, variables
(predicates), and blocked clauses. Our evaluation using the
Zipperposition prover confirms that the new techniques usefully
supplement the existing superposition machinery.
en
dc.language.iso
en
-
dc.relation.ispartofseries
Conference Series: Formal Methods in Computer-Aided Design
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
formal methods
en
dc.subject
computer-aided system design
en
dc.subject
hardware and system verification
en
dc.subject
formale Methode
de
dc.subject
rechnerunterstützte Systementwicklung
de
dc.subject
Hardwareverifikation
de
dc.title
SAT-Inspired Eliminations for Superposition
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34727/2021/isbn.978-3-85448-046-4_32
-
dc.contributor.affiliation
Vrije Universiteit Amsterdam, Netherlands (the)
-
dc.contributor.affiliation
Université de Lorraine, France
-
dc.contributor.affiliation
Carnegie Mellon University, United States of America (the)
-
dc.relation.isbn
978-3-85448-046-4
-
dc.relation.doi
10.34727/2021/isbn.978-3-85448-046-4
-
dc.description.volume
2
-
dc.description.startpage
231
-
dc.description.endpage
240
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
2708-7824
-
tuw.booktitle
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
-
tuw.peerreviewed
true
-
tuw.relation.ispartof
10.34727/2021/isbn.978-3-85448-046-4
-
tuw.relation.publisher
TU Wien Academic Press
-
tuw.relation.publisherplace
Wien
-
tuw.book.chapter
32
-
tuw.publication.orgunit
E000 - Technische Universität Wien
-
dc.identifier.libraryid
AC17204226
-
dc.description.numberOfPages
10
-
tuw.relation.ispartoftuwseries
Conference Series: Formal Methods in Computer-Aided Design
-
tuw.author.orcid
0000-0001-7049-6847
-
tuw.author.orcid
0000-0002-8367-0936
-
tuw.author.orcid
0000-0002-5587-8801
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openairetype
conference paper
-
item.fulltext
with Fulltext
-
item.mimetype
application/pdf
-
item.grantfulltext
open
-
crisitem.author.dept
Vrije Universiteit Amsterdam, Netherlands (the)
-
crisitem.author.dept
Université de Lorraine, France
-
crisitem.author.dept
Carnegie Mellon University, United States of America (the)
