<div class="csl-bib-body">
<div class="csl-entry">Bloem, R., Malik, S., Schlaipfer, M., & Weissenbacher, G. (2014). Reduction of Resolution Refutations and Interpolants via Subsumption. In E. Yahav (Ed.), <i>Hardware and Software: Verification and Testing : 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings</i>. Springer Cham. https://doi.org/10.1007/978-3-319-13338-6_15</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/354
-
dc.description
The final publication is available via <a href="https://doi.org/10.1007/978-3-319-13338-6_15" target="_blank">https://doi.org/10.1007/978-3-319-13338-6_15</a>.
-
dc.description.abstract
Propositional resolution proofs and interpolants derived from them are widely used in automated verification and circuit synthesis. There is a broad consensus that "small is beautiful"-small proofs and interpolants lead to concise abstractions in verification and compact designs in synthesis. Contemporary proof reduction techniques either minimise the proof during construction, or perform a post-hoc transformation of a given resolution proof. We focus on the latter class and present a subsumption-based proof reduction algorithm that extends existing singlepass analyses and relies on a meet-over-all-paths analysis to identify redundant resolution steps and clauses.We show that smaller refutations do not necessarily entail smaller interpolants, and use labelled interpolation systems to generalise our reduction approach to interpolants. Experimental results support the theoretical claims.
en
dc.description.sponsorship
Austrian Science Funds (FWF)
-
dc.language
English
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
https://creativecommons.org/licenses/by/4.0/
-
dc.title
Reduction of Resolution Refutations and Interpolants via Subsumption
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.relation.isbn
9783319133379
-
dc.relation.doi
10.1007/978-3-319-13338-6
-
dc.relation.issn
0302-9743
-
dc.relation.grantno
W1255-N23
-
dc.relation.grantno
S11408-N23
-
dc.rights.holder
Springer International Publishing Switzerland 2014
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Hardware and Software: Verification and Testing : 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014, Proceedings
-
tuw.container.volume
8855
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer Cham
-
tuw.version
am
-
tuw.publication.orgunit
E192 - Institut für Informationssysteme
-
tuw.publisher.doi
10.1007/978-3-319-13338-6_15
-
dc.identifier.libraryid
AC11362486
-
dc.description.numberOfPages
20
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:3-3031
-
tuw.author.orcid
0000-0002-1411-5744
-
dc.rights.identifier
CC BY 4.0
en
dc.rights.identifier
CC BY 4.0
de
tuw.event.name
10th International Haifa Verification Conference, HVC 2014
-
tuw.event.startdate
18-11-2014
-
tuw.event.enddate
20-11-2014
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Haifa
-
tuw.event.country
IL
-
tuw.event.presenter
Bloem, Roderick
-
item.fulltext
with Fulltext
-
item.grantfulltext
open
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.openaccessfulltext
Open Access
-
item.mimetype
application/pdf
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
