Automating the Knuth Bendix ordering

DOI10.1007/BF01237233zbMath0715.68044WikidataQ55393323 ScholiaQ55393323MaRDI QIDQ751830

John Kalmus, Jeremy Dick, Ursula Martin Webb

Publication date: 1990

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

completion algorithmKnuth-Bendix ordering

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Thue and Post systems, etc. (03D03)

Related Items

Linear interpretations by counting patterns, KBO orientability, Tyrolean termination tool: techniques and features, Simple termination of rewrite systems, An Extension of the Knuth-Bendix Ordering with LPO-Like Properties, Orienting rewrite rules with the Knuth-Bendix order., An upper bound on the derivational complexity of Knuth-Bendix orderings., The order types of termination orderings on monadic terms, strings and multisets, Termination of term rewriting using dependency pairs, Derivation lengths and order types of Knuth--Bendix orders, Decision Procedures for Automating Termination Proofs, Transforming SAT into Termination of Rewriting, Invariants, patterns and weights for ordering terms, Modular termination proofs for rewriting using dependency pairs, Generating polynomial orderings

Uses Software

• REVE

Cites Work

• Termination of rewriting systems by polynomial interpretations and its implementation
• Orderings for term-rewriting systems
• Termination of rewriting
• Rewriting systems on FP expressions to reduce the number of sequences yielded
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Systems of predicative analysis, II: Representations of ordinals
• Ordering by Divisibility in Abstract Algebras
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item