License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.174
URN: urn:nbn:de:0030-drops-40616
URL: http://drops.dagstuhl.de/opus/volltexte/2013/4061/
Go to the corresponding LIPIcs Volume Portal


Felgenhauer, Bertram ; van Oostrom, Vincent

Proof Orders for Decreasing Diagrams

pdf-format:
14.pdf (0.7 MB)


Abstract

We present and compare some well-founded proof orders for decreasing diagrams. These proof orders order a conversion above another conversion if the latter is obtained by filling any peak in the former by a (locally) decreasing diagram. Therefore each such proof order entails the decreasing diagrams technique for proving confluence. The proof orders differ with respect to monotonicity and complexity. Our results are developed in the setting of involutive monoids. We extend these results to obtain a decreasing diagrams technique for confluence modulo.

BibTeX - Entry

@InProceedings{felgenhauer_et_al:LIPIcs:2013:4061,
  author =	{Bertram Felgenhauer and Vincent van Oostrom},
  title =	{{Proof Orders for Decreasing Diagrams}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{174--189},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4061},
  URN =		{urn:nbn:de:0030-drops-40616},
  doi =		{10.4230/LIPIcs.RTA.2013.174},
  annote =	{Keywords: involutive monoid, confluence modulo, decreasing diagram, proof order}
}

Keywords: involutive monoid, confluence modulo, decreasing diagram, proof order
Seminar: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 14.06.2013


DROPS-Home | Fulltext Search | Imprint Published by LZI