[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Nachum Dershowitz
Date: June 1993
Summary: Is confluence of ordered rewriting decidable when the (existential fragment of the) ordering is?
Is confluence of ordered rewriting (using the intersection of one step replacement of equals and a reduction ordering that is total on ground terms) decidable when the (existential fragment of the) ordering is? This question was raised in [Nie93], where some results were given for the lexicographic path ordering.
This was answered positive for the case of lexicographic path orderings, which is probably the most important special case, in [CNNR98]. The general question, however, remains open.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |