6533b829fe1ef96bd12897d4

RESEARCH PRODUCT

Incremental termination proofs and the length of derivations

Clemens LautemannFrank Drewes

subject

Discrete mathematicsCombinatoricsTermination proofPolynomial complexityRewriting systemWord problem (mathematics)Mathematical proofComputer Science::DatabasesMathematics

description

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.

yearjournalcountryeditionlanguage
1991-01-01
https://doi.org/10.1007/3-540-53904-2_85