An efficient and flexible approach to resolution proof reduction

DOI10.1007/978-3-642-19583-9_17MaRDI QIDQ5391528zbMATH OpenOpenAlexFDO

Authors Simone Fulvio Rollini, Roberto Bruttomesso, Natasha Sharygina

Publication date 6 April 2011

Published in Hardware and Software: Verification and Testing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19583-9_17

Mathematics Subject Classification ID

Recommendations

• Improved single pass algorithms for resolution proof reduction
• Two techniques for minimizing resolution proofs
• Resolution proof transformation for compression and interpolation
• Data compression for proof replay
• Compressing propositional refutations

Cited in

(16)

• Structuring resolution proofs by introducing new lemmata or how to improve the readability of ATP-generated proofs
• Exploiting partial variable assignment in interpolation-based model checking
• Andrews Skolemization may shorten resolution proofs non-elementarily
• Mining propositional simplification proofs for small validating clauses
• Guiding Craig interpolation with domain-specific abstractions
• Analysis of a new reduction calculus for the satisfiability problem
• Towards the compression of first-order resolution proofs by lowering unit clauses
• Boundary Points and Resolution
• Improved single pass algorithms for resolution proof reduction
• Resolution proof transformation for compression and interpolation
• Two techniques for minimizing resolution proofs
• Compressing propositional refutations
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
• Efficient generation of small interpolants in CNF
• Proof optimization for partial redundancy elimination
• Optimization techniques for Craig interpolant compaction in unbounded model checking

This page was built for publication: An efficient and flexible approach to resolution proof reduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5391528)