Padawitz, Peter Strategy-controlled reduction and narrowing. (English) Zbl 0635.68105 Rewriting techniques and applications, Proc. 2nd Int. Conf., Bordeaux/France 1987, Lect. Notes Comput. Sci. 256, 242-252 (1987). [For the entire collection see Zbl 0619.00025.] 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. Cited in 1 Document MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B35 Mechanization of proofs and logical operations Keywords:inference rules; reduction; narrowing; atomic formulas; selection of redices; Church-Rosser properties; Horn clause specification; completeness; strategy independence; uniformity Citations:Zbl 0619.00025 PDFBibTeX XML