cl-banner

A Proof Order for Decreasing Diagrams

Bertram Felgenhauer

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

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.

 

  PDF

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
}
Nach oben scrollen