An upper bound on the derivational complexity of Knuth-Bendix orderings.

DOI10.1016/S0890-5401(03)00008-7zbMath1055.68063MaRDI QIDQ1401942

Dieter Hofbauer

Publication date: 19 August 2003

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

Knuth-Bendix orderTerm rewritingDerivational complexityTermination proofs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Uses Software

• EXPANDER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• Automating the Knuth Bendix ordering
• Systems of reductions
• Ordinal recursive bounds for Higman's theorem
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• On a conjecture of Yves Métivier
• Termination of term rewriting: Interpretation and type elimination
• Simply terminating rewrite systems with long derivations
• Complexity bounds for some finite forms of Kruskal's theorem
• Calcul de longueurs de chaînes de réécriture dans le monoïde libre
• Deduction and Declarative Programming
• Termination proofs and the length of derivations
• Time bounded rewrite systems and termination proofs by generalized embedding
• Derivation lengths and order types of Knuth--Bendix orders

This page was built for publication: An upper bound on the derivational complexity of Knuth-Bendix orderings.