DSpace Repository

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

Files in this item

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

Abstract

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.^^^^

Type:

Article

xmlui.dri2xhtml.METS-1.0.item-indexacio:

 
Indexat a SCOPUS
 
Indexat a WOS/JCR
 

Rights:

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

Citation:

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