Abstract

This paper improves the existing criterion for proving confluence of a normal conditional term rewriting system (CTRS) via the Serbanuta-Rosu transformation, a computationally equivalent transformation of CTRSs into unconditional term rewriting systems (TRS), showing that a weakly left-linear constructor normal CTRS is confluent if the transformed TRS is confluent. Then, we discuss usefulness of the optimization of the Serbanuta-Rosu transformation, which has been discussed in the literature.

BibTeX

@inproceedings{NNMYKG-IWC14,
  author    = "Naoki Nishida and Makashi Yanagisawa and Karl Gmeiner",
  title     = "On Proving Confluence of Conditional Term Rewriting Systems
               via the Computationally Equivalent Transformation",
  booktitle = "Proceedings of the 3rd International Workshop on Confluence",
  editor    = "Takahito Aoto and Delia Kesner",
  pages     = "24--28",
  year      = 2014
}