Abstract
Incremental termination proofs, a concept similar to termination proofs by quasi-commuting orderings, are investigated. In particular, we show how an incremental termination proof for a term rewriting system T can be used to derive upper bounds on the length of derivations in T. A number of examples show that our results can be applied to yield (sharp) low-degree polynomial complexity bounds.
Cite
CITATION STYLE
Drewes, F., & Lautemann, C. (1991). Incremental termination proofs and the length of derivations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 488 LNCS, pp. 49–61). Springer Verlag. https://doi.org/10.1007/3-540-53904-2_85
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
