Narrowing

Abstract

The Narrowing Rule is both a specialization of the Paramodulation Rule (cf. Section 5.3) and a generalization of the Single (goal) Reduction Rule (cf. Section 7.7). As a particular case of paramodulation narrowing applies conditional equations only from left to right and instantiates a goal only by irreducible substi tut ions. Wi th regard to goal reduction, narrowi ng adds the possibility of substituting into the variables of a goal before reducing it. However, the restriction to irreducible substitutions implies that a goal, say γ, can be narrowed only if it already contains some proper prefix of a reduction redex. An instantiation of γ is to complete the prefix to the full redex. “Proper” means that the prefix must not be a variable. Therefore reduction redices cannot be generated arbitrarily, just by substituting left-hand sides of conditional equations into variables of γ. Consequently, the number of possible narrowing steps starting out from γ is considerably smaller than the number of paramodulants of γ, even if we confine ourselves to most general paramodulation.