Content deleted Content added
Add category |
m →top: clean up spacing around commas and other punctuation fixes, replaced: ; → ; (8) |
||
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 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==
| |||