×

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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations

Citations:

Zbl 0619.00025