[Submit a comment] [RTALooP home] [Index] [Previous] [Next]  [Postscript] [PDF] [BibTeX Source] [LaTeX Source] 
Originator: Yoshihito Toyama
Date: April 1991
Summary: Under what conditions does confluence of a normal semiequational conditional term rewriting system imply confluence of the associated oriented system?
For a normal conditional termrewriting system R = { s →^{!} t ⇒ l → r }, where t must be a ground normal from of s, we can consider the corresponding semiequational conditional rewrite system R_{se} = { s ↔^{*} t ⇒ l → r }. Under what conditions does confluence of R_{se} imply confluence of R? In general, this is not the case, as can be seen from the following nonconfluent system R (due to Aart Middeldorp):

Solutions have been provided by [YASM00]. They show that confluence of R follows from confluence of R_{se} if any of the two following conditions is satisfied:
See [YASM00] for definitions of these properties.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next]  [Postscript] [PDF] [BibTeX Source] [LaTeX Source] 