Resolution proof reduction via local context rewriting: Difference between revisions

Revision as of 05:53, 3 April 2012

Revision as of 05:56, 3 April 2012

Line 1:

A technique for resolution proof reduction via local context rewriting was proposed by Simone Rollini, Roberto Bruttomesso and Natasha Sharygina in their paper "An Efficient and Flexible Approach to Resolution Proof Reduction"<ref name=Simone>Simone, S.F. ; Brutomesso, R. ; Sharygina, N. "An Efficient and Flexible Approach to Resolution Proof Reduction". 6th Haifa Verification Conference, 2010.</ref>. This [[proof compression]] method was presented as an algorithm named ReduceAndReconstruct, by the authors. ReduceAndReconstructthat operates as a post-processingprocess on [[resolution (logic)|resolution]] proofs.

ReduceAndReconstruct is based on a set of local proof rewriting rules that transform a subproof into a equivalent or stronger one <ref name=Simone />. Each rule is defined to match a specific context.