Skip to main content

Reduction of resolution refutations and interpolants via subsumption

Author(s): Bloem, R; Malik, S; Schlaipfer, M; Weissenbacher, G

To refer to this page use:
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.
Publication Date: 2014
Citation: Bloem, R, Malik, S, Schlaipfer, M, Weissenbacher, G. (2014). Reduction of resolution refutations and interpolants via subsumption. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8855 (188 - 203
Pages: 188 - 203
Type of Material: Conference Article
Journal/Proceeding Title: Lecture Notes in Computer Science
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.