[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #64

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.

Remark

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.

References

[CNNR98]

Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, and Michaël Rusinowitch. Decision problems in ordered rewriting. In Vaughan Pratt, editor, Thirteenth IEEE Annual Symposium on Logic in Computer Science, Indianapolis, IN, June 1998. IEEE.

[Nie93]

Robert Nieuwenhuis. A precedence-based total AC-compatible ordering. In Claude Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, pages 374–388, Montreal, Canada, June 1993. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]