Resolution proof reduction via local context rewriting: Difference between revisions

Revision as of 18:54, 25 September 2014

Revision as of 22:56, 11 October 2014

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 ReduceAndReconstruct 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.