Abstract

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.

BibTeX

@inproceedings{BF-IWC12,
  author      = "Bertram Felgenhauer",
  title       = "A Proof Order for Decreasing Diagrams",
  booktitle   = "Proceedings of the 1st International Workshop on
                 Confluence",
  pages       = "7--13",
  year        = 2012
}