Restrictions for Inferences.

Given an ordering and a selection function, the chaining inferences are restricted in that an inference is performed only between maximal or selected atoms in a clause, and only if the middle term through which is being chained is maximal (with respect to the given reduction ordering $\succ$) in both atoms:

1. $s\sigma \not\succeq t\sigma$,
2. $v\sigma \not\succeq u\sigma$,
3. the participating $R$-atoms must either be maximal or selected within the repsective premises; and
4. the positive (that is, first) premise of an inference contains no selected literals.

Hence, selection not only indicates which subgoal to solve in a clause. It also serves to block clauses from becoming a positive premise in an inference.

Unrestricted chaining amounts to hyperresolution with the transitivity axiom and creates a large search space. This is illustrated by the two examples HRES15 and OC15 which both consist of the facts $i > i+1$, for $i=1,\ldots,14$, together with the transitivity axiom for $>$. In the case of HRES15, the ordering restrictions are turned off. To saturate HRES15 takes about 100 times longer than running the example in the unsual ordered chaining mode OC15.

Imprint | Data Protection