Strategy-controlled reduction and narrowing

Abstract

The inference rules "reduction" and "narrowing" are generalized from terms resp equations to arbitrary atomic formulas. Both rules are parameterized by strategies to control the selection of redices. Church-Rosser properties of the underlying Horn clause specification are shown to ensure both completeness and strategy independence of reduction. "Uniformity" turns out as the crucial property of those reduction strategies which serve as complete narrowing strategies. A characterization of uniformity (and hence completeness) of leftmost-outermost narrowing is presented.