Content deleted Content added
Mark viking (talk | contribs) →top: c/e, remove some promotional mentions and informal tone |
m →top: clean up spacing around commas and other punctuation fixes, replaced: ; → ; (8) |
||
| (3 intermediate revisions by 3 users 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.
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.
* 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 63:
</math>|{{EquationRef|3}}}}
The proof is now illegal because the literal <math>o</math> is missing from the transformed root clause. To reconstruct the proof, one can remove <math>o</math> together with the last resolution step (that is now
{{NumBlk|:|
Line 70:
</math>|{{EquationRef|4}}}}
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.
==Notes==
{{reflist}}
[[Category:Articles with example pseudocode]]
[[Category:Proof theory]]
| |||