×

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

MSC:

68Q65 Abstract data types; algebraic specification
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q55 Semantics in the theory of computing

Citations:

Zbl 0533.00025