×

A total, ground path ordering for proving termination of AC-rewrite systems. (English) Zbl 1379.68197

Comon, Hubert (ed.), Rewriting techniques and applications. 8th international conference, RTA ’97, Sitges, Spain, June 2–5, 1997. Proceedings. Berlin: Springer (ISBN 978-3-540-62950-4/pbk; 978-3-540-69051-1/ebook). Lecture Notes in Computer Science 1232, 142-156 (1997).
Summary: 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.
For the entire collection see [Zbl 1360.68009].

MSC:

68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI