It is undecidable in general whether or not a term-rewriting system is confluent on a given congruence class. This result is shown to hold even when the term-rewriting systems under consideration contain unary function symbols only, and all their rules are length-reducing. On the other hand, for certain subclasses of these systems confluence on a given congruence class is decidable.
CITATION STYLE
Otto, F. (1987). Some results about confluence on a given congruence class. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 256 LNCS, pp. 145–155). Springer Verlag. https://doi.org/10.1007/3-540-17220-3_13
Mendeley helps you to discover research relevant for your work.