A Proof Order for Decreasing Diagrams

Bertram Felgenhauer

Proceedings of the 1st International Workshop on Confluence (IWC 2012), pp. 7 – 13, 2012.


In this note we describe a well-founded proof order that entails the decreasing diagrams technique, i.e., it orders peaks of locally
decreasing diagrams above their joining sequences. We also investigate an extension that promises to be useful for proving confluence modulo.
Unrelated to this proof order we also present an example showing that witnesses for non-confluence can not always be found by starting from critical pairs alone, even for linear TRSs.




author = "Bertram Felgenhauer",
title = "A Proof Order for Decreasing Diagrams",
booktitle = "Proceedings of the 1st International Workshop on Confluence",
pages = "7--13",
year = 2012
Nach oben scrollen