← All problems
Unverified
Is confluence of ordered rewriting decidable when the (existential fragment of the) ordering is?
The source page states the original problem together with its recorded qualifications and progress updates as follows.
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 [Dershowitz, 1993], where some results were given for the lexicographic path ordering.
Recorded progress.
This was answered positive for the case of lexicographic path orderings, which is probably the most important special case, in [Dershowitz, 1993]. The general question, however, remains open.
