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

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.