Derivation lengths and order types of Knuth--Bendix orders

DOI10.1016/S0304-3975(01)00015-9zbMath0983.68087MaRDI QIDQ5958622

Ingo Lepper

Publication date: 3 March 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

Ackermann functionderivation lengthfast growing functionsKnuth-Bendix orderorder type

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (7)

KBO orientability ⋮ An upper bound on the derivational complexity of Knuth-Bendix orderings. ⋮ Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations ⋮ The Hydra battle and Cichon's principle ⋮ 2004 Summer Meeting of the Association for Symbolic Logic ⋮ Complexity Analysis by Rewriting ⋮ The Derivational Complexity Induced by the Dependency Pair Method

Cites Work

• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• Automating the Knuth Bendix ordering
• Termination of rewriting
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Some results on cut-elimination, provable well-orderings, induction and reflection
• Simply terminating rewrite systems with long derivations
• Complexity bounds for some finite forms of Kruskal's theorem
• Proof-theoretic analysis of termination proofs
• Termination proofs and the length of derivations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Derivation lengths and order types of Knuth--Bendix orders