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