2003 | OriginalPaper | Buchkapitel
Monotonic AC-Compatible Semantic Path Orderings
verfasst von : Cristina Borralleras, Albert Rubio
Erschienen in: Rewriting Techniques and Applications
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Polynomial interpretations and RPO-like orderings allow one to prove termination of Associative and Commutative (AC-)rewriting by only checking the rules of the given rewrite system. However, these methods have important limitations as termination proving tools.To overcome these limitations, more powerful methods like the dependency pair method have been extended to the AC-case. Unfortunately, in order to ensure AC-termination, the so-called extended rules, which, in general, are hard to prove, must be added to the rewrite system.In this paper we present a fully monotonic AC-compatible semantic path ordering. This monotonic AC-ordering defines a new automatable termination proving method for AC-rewriting which does not need to consider extended rules. As a hint of the power of this method, we can easily prove several non-trivial examples appearing in the literature, including one that, to our knowledge, can be handled by no other automatic method.