DSpace/Dipòsit Manakin

The recursive path and polynomial ordering for first-order and higher-order terms

The recursive path and polynomial ordering for first-order and higher-order terms
 
Bofill, Miquel ; Borralleras Andreu, Cristina ; Rodríguez-Carbonell, Enric ; Rubio, Albert
06-2012

Text complet d'aquest document

Icon
Nom: artconlli_a2012_bofill_miquel_recursive_path_polynomial.pdf
Mida: 742.8Kb
Format: PDF
Descripció: Només administradors
Enllaç permanent: http://hdl.handle.net/10854/2144
 
Versió de l'editor: https://doi.org/10.1093/logcom/exs027
 

Resum:

In most termination tools two ingredients, namely recursive path orderings (RPOs) and polynomial interpretation orderings (POLOs), are used in a consecutive disjoint way to solve the final constraints generated from the termination problem. In this article we present a simple ordering that combines both RPO and POLO and defines ...»»»»
In most termination tools two ingredients, namely recursive path orderings (RPOs) and polynomial interpretation orderings (POLOs), are used in a consecutive disjoint way to solve the final constraints generated from the termination problem. In this article we present a simple ordering that combines both RPO and POLO and defines a family of orderings that includes both, and extend them with the possibility of having, at the same time, an RPO-like treatment for some symbols and a POLO-like treatment for the others. The ordering is extended to higher-order terms, providing a new fully automatable use of polynomial interpretations in combination with beta-reduction.^^^^

Tipus:

Article

Indexació:

 
Indexat a SCOPUS
 
Indexat a WOS/JCR
 

Drets:

 
(c) Oxford University Press, 2012
 
Tots els drets reservats
 

Citació Bibliogràfica:

Miquel Bofill, Cristina Borralleras, Enric Rodríguez-Carbonell, and Albert Rubio. The recursive path and polynomial ordering for first-order and higher-order terms J Logic Computation (2013) 23(1): 263-305 first published online June 22, 2012 doi:10.1093/logcom/exs027