Abstract
Knuth and Bendix showed that confluence of a terminating first-order rewrite system can be reduced to the joinability of its finitely many critical pairs. We show that this is still true of a rewrite system such that is terminating and is a left-linear, rank non-increasing, possibly non-terminating rewrite system. Confluence can then be reduced to the joinability of the critical pairs of and to the existence of decreasing diagrams for the critical pairs of inside as well as for the rigid parallel critical pairs of. © 2014 Springer International Publishing Switzerland.
Cite
CITATION STYLE
Liu, J., Dershowitz, N., & Jouannaud, J. P. (2014). Confluence by critical pair analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 287–302). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_20
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
