Perdrix, H. Propriétés Church-Rosser de systèmes de réecriture equationnels ayant la propriété de termination faible. (French) Zbl 0583.68005 Theoretical aspects of computer science, Symp., Paris 1984, Lect. Notes Comput. Sci. 166, 97-108 (1984). [For the entire collection see Zbl 0533.00025.] The problem of proving and characterizing the Church-Rosser property of term rewriting systems is of basic importance in a non-resolution theorem proving methodology. The author shows various theorems which allow to derive the validity of the confluence given a set of rewriting rules ”weakly terminating”. He extends some results already known in the literature by assuming that the termination of the rewriting rules holds without considering a specified set of equations. Reviewer: A.Pettorossi Cited in 3 Documents MSC: 68Q65 Abstract data types; algebraic specification 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68Q55 Semantics in the theory of computing Keywords:equational theories; unification; Church-Rosser property; term rewriting systems; non-resolution theorem proving; confluence; termination Citations:Zbl 0533.00025 PDFBibTeX XML