cl-banner

On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation

Naoki Nishida, Makashi Yanagisawa, and Karl Gmeiner

Proceedings of the 3rd International Workshop on Confluence (IWC 2014), pp. 24 – 28, 2014.

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.

 

  PDF

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