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.

Models of Computation (acm F.1.1), Grammars and Other Rewriting Systems (acm F.4.2)
Grammars and rewriting systems (msc 68Q42), dimensions (msc 52C20)
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. Software Engineering [SEN]. CWI.