DSpace/Dipòsit Manakin

Monotonic AC-Compatible Semantic Path Orderings

Monotonic AC-Compatible Semantic Path Orderings
 
Borralleras Andreu, Cristina ; Rubio, Albert
2003

Text complet d'aquest document

Icon
Nom: artconlli_a2003_borralleras_cristina_monotonic.pdf
Mida: 216.8Kb
Format: PDF
Descripció: Només accés administradors
Enllaç permanent: http://hdl.handle.net/10854/1893
 

Resum:

Abstract. Polynomial interpretations and RPO-like orderings allow one to prove termination of Associative and Commutative (AC-)rewriting by only checkingthe rules of the given rewrite system. However, these methods have important limitations as termination provingto ols. To overcome these limitations, more powerful methods ...»»»»
Abstract. Polynomial interpretations and RPO-like orderings allow one to prove termination of Associative and Commutative (AC-)rewriting by only checkingthe rules of the given rewrite system. However, these methods have important limitations as termination provingto ols. 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, CA gpApirμj rip hrio nO RiO/pj >skn bp roopo nO nhp ipwiCnp kaknp>. In this paper we present a fully monotonic AC-compatible semantic path ordering. This monotonic AC-orderingdefines a new automatable termination provingmetho d for AC-rewritingwhic h does not need to consider extended rules. As a hint of the power of this method, we can easily prove several non-trivial examples appearingin the literature, includingone that, to our knowledge, can be handled by no other automatic method.^^^^

Tipus:

Capítol o part de llibre

Drets:

 
(c) Springer
 
Tots els drets reservats
 

Citació Bibliogràfica:

BORRALLERAS ANDREU, Cristina; RUBIO, A. Monotonic AC-compatible semantic path orderings. Valencia, Spain, Berlin, Germay: Spinger-Verlag Berlin, 2003..