Content deleted Content added
sp |
Add category |
||
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 112:
{{reflist}}
[[Category:Articles with example pseudocode]]
[[Category:Proof theory]]
| |||