Resolution proof reduction via local context rewriting: Difference between revisions

Revision as of 16:44, 13 April 2012

Revision as of 21:17, 16 January 2013

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 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, that operates as a post-process 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.

A context (as defined by Simone ''et al.'' <ref name=Simone />) involves two pivots (<math>p</math> and <math>q</math>) and five clauses (<math>\alpha</math>, <math>\beta</math>, <math>\gamma</math>, <math>\delta</math> and <math>\eta</math>). The structure of a context is shown in ({{EquationNote|1}}). Note that this imply that <math>p</math> is contained in <math>\beta</math> and <math>\gamma</math> (with opposite polarity) and <math>q</math> is contained in <math>\delta</math> and <math>\alpha</math> (also with opposite polarity).

Line 7:

{{NumBlk|:|<math>\cfrac{\cfrac{\beta \qquad \gamma}{\delta} \, p \qquad \alpha}{\eta} \, q</math>|{{EquationRef|1}}}}

The table below shows the rewriting rules proposed by Simone ''et al.'' .<ref name=Simone />. The idea of the algorithm is to reduce proof size by opportunistically applying these rules.

{| class="wikitable"

Line 42:

|}

Note that the first five rules were introduced in a 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, the following is worth mentioning:

* 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 82:

7 '''end function'''

ReduceAndReconstruct uses the function ReduceAndReconstructLoop, which is specified below. Note that 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 103:

18 '''end function'''

Another point that worth mentioning is that if the input proof is not a tree (in general, resolution graphs are [[directed acyclic graph|directed acyclic graphs]]s), then the clause <math>\delta</math> of a context may be involved in more than one resolution step. In this case, to ensure that a application of a rewriting rule is not going to interfere with other resolution steps, a safe solution is to create a copy of the node represented by clause <math>\delta</math> .<ref name=Simone />. Note that this solution increases proof size and some caution is needed when doing this.

Moreover, 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==