A new path ordering for showing termination of associative-commutative (AC) rewrite systems is defined. If the precedence relation on function symbols is total, the ordering is total on ground terms, but unlike the ordering proposed by Rubio and Nieuwenhuis, this ordering can orient the distributivity property in the proper direction. The ordering is defined in a natural way using recursive path ordering with status as the underlying basis. This settles a longstanding problem in termination orderings for AC rewrite systems. The ordering can be used to define an ordering on nonground terms.
CITATION STYLE
Kapur, D., & Sivakumar, G. (1997). A total, ground path ordering for proving termination of AC-rewrite systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1232, pp. 142–156). Springer Verlag. https://doi.org/10.1007/3-540-62950-5_67
Mendeley helps you to discover research relevant for your work.