%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Miquel Bofill at 2013-01-23 13:26:25 +0100 


%% Saved with string encoding Unicode (UTF-8) 



@article{BofillBRR13JLC,
	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 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.},
	Author = {Bofill, Miquel and Borralleras, Cristina and Rodr{\'\i}guez-Carbonell, Enric and Rubio, Albert},
	Date-Modified = {2013-01-23 12:25:55 +0000},
	Doi = {10.1093/logcom/exs027},
	Eprint = {http://logcom.oxfordjournals.org/content/23/1/263.full.pdf+html},
	Journal = {Journal of Logic and Computation},
	Number = {1},
	Pages = {263-305},
	Title = {The recursive path and polynomial ordering for first-order and higher-order terms},
	Url = {http://logcom.oxfordjournals.org/content/23/1/263.abstract},
	Volume = {23},
	Year = {2013},
	Bdsk-Url-1 = {http://logcom.oxfordjournals.org/content/23/1/263.abstract},
	Bdsk-Url-2 = {http://dx.doi.org/10.1093/logcom/exs027}}