Resolution proof reduction via local context rewriting: Difference between revisions

Revision as of 23:46, 2 November 2014

Latest revision as of 14:48, 16 January 2024

(One intermediate revision by one other user not shown)

Line 1:

In [[proof theory]], an area of [[mathematical logic]], '''resolution proof reduction via local context rewriting''' is a technique for resolution [[proof compression|proof reduction]] via local context [[rewriting]].<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'', that operates as a post-processing of [[resolution (logic)|resolution]] proofs.

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

Line 42:

|}

The first five rules were introduced in an earlier paper.<ref name=Bruttomesso>Bruttomesso, R. ; Rollini, S. ; Sharygina, N.; Tsitovich, A. "Flexible Interpolation with Local Proof Transformations". The International Conference on Computer-Aided Design, 2010.</ref> In addition:

* Rule A2 does not perform any reduction on its own. However, it is still useful, because of its "shuffling" effect that can create new opportunities for applying the other rules;

Line 72:

A further reduction of this proof by applying rule A2 to create a new opportunity to apply rule B2'.<ref name=Simone />

There are usually a huge number of contexts where rule A2 may be applied, so an exhaustive approach is not feasible in general. One proposal<ref name=Simone /> is to execute <code>ReduceAndReconstruct</code> as a loop with two termination criteria: number of iterations and a timeout (what is reached first). The pseudocode<ref name=Simone /> below shows this.

1 '''function''' ReduceAndReconstruct(''<math>\pi</math>'' ''/* a proof */'', ''timelimit'', ''maxIterations''):

Line 82:

7 '''end function'''

<code>ReduceAndReconstruct</code> uses the function <code>ReduceAndReconstructLoop</code>, which is specified below. The first part of the algorithm does a [[topological ordering]] of the [[resolution graph]] (considering that edges goes from antecedentes to resolvents). This is done to ensure that each node is visited after its antecedents (this way, broken resolution steps are always found and fixed).<ref name=Simone />

1 '''function''' ReduceAndReconstructLoop(''<math>\pi</math>'' ''/* a proof */''):

Line 107:

The [[heuristic]] for rule selection is important to achieve a good compression performance. Simone ''et al.'' <ref name=Simone /> use the following order of preference for the rules (if applicable to the given context): B2 > B3 > { B2', B1 } > A1' > A2 (X > Y means that X is preferred over Y).

Experiments have shown that ReduceAndReconstruct alone has a worse compression/time ratio than the algorithm [[RecyclePivots]].<ref name=Bar-Ilan>Bar-Ilan, O. ; Fuhrmann, O. ; Hoory, S. ; Shacham, O. ; Strichman, O. "Linear-Time Reductions of Resolution Proofs". HVC, 2008.</ref> However, while RecyclePivots can be applied only once to a proof, ReduceAndReconstruct may be applied multiple times to produce a better compression. An attempt to combine ReduceAndReconstruct and RecyclePivots algorithms has led to good results.<ref name=Simone />

==Notes==

{{reflist}}

[[Category:Articles with example pseudocode]]

[[Category:Proof theory]]