WeU-foundedncss is the essential property of orderings for proving termination. We introduce a simple criterion on term orderings such that any term ordering possessing the subterm property and satisfying this criterion is wen-founded. The usual path orders fulfil this criterion, yielding a much simpler proof of well-foundedness than the classical proof depending on Kruskal's theorem. Even more, our approach covers non-simplification orders like spo and gpo which can not be dealt with by Kruskal's theorem. For finite alphabets we present completeness results, i. e., a term rewriting system terminates if and only if it is compatible with an order satisfying the criterion. For infinite alphabets the same completeness results hold for a slightly different criterion.
CITATION STYLE
Ferreira, M. C., & Zantema, H. (1995). Well-foundedness of term orderings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 968, pp. 106–123). Springer Verlag. https://doi.org/10.1007/3-540-60381-6_7
Mendeley helps you to discover research relevant for your work.