TY - CHAP
T1 - Reduction of resolution refutations and interpolants via subsumption
AU - Bloem, Roderick
AU - Malik, Sharad
AU - Schlaipfer, Matthias
AU - Weissenbacher, Georg
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2014.
PY - 2014
Y1 - 2014
N2 - 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 ameet-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.
AB - 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 ameet-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.
UR - http://www.scopus.com/inward/record.url?scp=84921342682&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84921342682&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-13338-6_15
DO - 10.1007/978-3-319-13338-6_15
M3 - Chapter
AN - SCOPUS:84921342682
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 188
EP - 203
BT - Hardware and Software
A2 - Yahav, Eran
PB - Springer Verlag
ER -