The criterion for confluence using decreasing diagrams is a generalization of several well-known confluence criteria in abstract rewriting, such as the strong confluence lemma. We give a new proof of the decreasing diagram theorem based on a geometric study of infinite reduction diagrams, arising from unsuccessful attempts to obtain a confluent diagram by tiling with elementary diagrams.

,
,
CWI
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

Klop, J. W., van Oostrom, V.& de Vrijer, R. (2000). A geometric proof of confluence by decreasing diagrams. In Software Engineering [SEN] (R 0007). CWI.