Abstract
We define a new path order ≺ POP so that for a finite rewrite system R compatible with ≺ POP, the complexity or derivation length function Dl Rf for each function symbol f is guaranteed to be bounded by a polynomial in the length of the inputs. Our results yield a simplification and clarification of the results obtained by Beckmann and Weiermann (Archive for Mathematical Logic, 36:11-30, 1996). © Springer-Verlag Berlin Heidelberg 2005.
Author supplied keywords
Cite
CITATION STYLE
Arai, T., & Moser, G. (2005). Proofs of termination of rewrite systems for polytime functions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3821 LNCS, pp. 529–540). https://doi.org/10.1007/11590156_43
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
