Orienting rewrite rules with the Knuth-Bendix order.

DOI10.1016/S0890-5401(03)00021-XzbMath1054.68079MaRDI QIDQ1401932

Andrei Voronkov, Konstantin Korovin

Publication date: 19 August 2003

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

zbMATH Keywords

TerminationTerm rewritingKnuth-Bendix ordersOrdering constraintsOrientability

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

KBO orientability, Tyrolean termination tool: techniques and features, AC-KBO revisited, αCheck: A mechanized metatheory model checker, Towards automated deduction in cP systems, On Transfinite Knuth-Bendix Orders, Completeness and Herbrand theorems for nominal logic, Transforming SAT into Termination of Rewriting, The size-change principle and dependency pairs for termination of term rewriting

Cites Work

• Simple LPO constraint solving methods
• Automating the Knuth Bendix ordering
• On recursive path ordering
• Invariants, patterns and weights for ordering terms
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item