Abstract

We show how to use the commutation version of van Oostrom’s decreasing diagrams for labeling left-linear term rewriting systems, based on Zankl et al.’s labeling framework. The resulting confluence criterion requires joining simultaneous critical pairs decreasingly, subsuming the criterion by Okui.

BibTeX

@inproceedings{BF-IWC15c,
  author    = "Bertram Felgenhauer",
  title     = "Labeling Multi-Steps for Confluence of Left-Linear Term
               Rewrite Systems",
  booktitle = "Proceedings of the 4th International Workshop on Confluence",
  editor    = "Ashish Tiwari and Takahito Aoto",
  pages     = "33--37",
  year      = 2015
}