Automating the Knuth Bendix ordering

DOI10.1007/BF01237233MaRDI QIDQ751830zbMATH OpenDBLPWikidataFDO

Authors Jeremy Dick, John Kalmus, Ursula Martin Webb

Publication date 1990

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF01237233

zbMATH Keywords

completion algorithmKnuth-Bendix ordering

Mathematics Subject Classification ID

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

Review text

The paper describes an algorithm that automatically constructs a Knuth- Bendix ordering for a finite system of terms rewriting rules if one such exists. The algorithm is based on a practical and simple algorithm to solve systems of linear inequalities.

Recommendations

• scientific article; zbMATH DE number 4041334
• scientific article; zbMATH DE number 3926235
• Things to know when implementing KBO
• Orienting rewrite rules with the Knuth-Bendix order.
• An AC-compatible Knuth-Bendix order.

Cites work

• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• scientific article; zbMATH DE number 3148887 (Why is no real title available?)
• scientific article; zbMATH DE number 3168109 (Why is no real title available?)
• scientific article; zbMATH DE number 3921958 (Why is no real title available?)
• scientific article; zbMATH DE number 3921961 (Why is no real title available?)
• scientific article; zbMATH DE number 4041334 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3497901 (Why is no real title available?)
• scientific article; zbMATH DE number 1988961 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3185418 (Why is no real title available?)
• Ordering by Divisibility in Abstract Algebras
• Orderings for term-rewriting systems
• Rewriting systems on FP expressions to reduce the number of sequences yielded
• Systems of predicative analysis, II: Representations of ordinals
• Termination of rewriting
• Termination of rewriting systems by polynomial interpretations and its implementation

Cited in

(22)

• Generating polynomial orderings
• Simple termination of rewrite systems
• Orienting rewrite rules with the Knuth-Bendix order.
• An upper bound on the derivational complexity of Knuth-Bendix orderings.
• Invariants, patterns and weights for ordering terms
• Modular termination proofs for rewriting using dependency pairs
• Termination of term rewriting using dependency pairs
• A Knuth-Bendix-like ordering for orienting combinator equations
• scientific article; zbMATH DE number 1722704 (Why is no real title available?)
• Decision Procedures for Automating Termination Proofs
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• scientific article; zbMATH DE number 3926235 (Why is no real title available?)
• scientific article; zbMATH DE number 4041334 (Why is no real title available?)
• The order types of termination orderings on monadic terms, strings and multisets
• Transforming SAT into termination of rewriting
• Linear interpretations by counting patterns
• Derivation lengths and order types of Knuth--Bendix orders
• A Formalization of Knuth–Bendix Orders
• A Formalization of Weighted Path Orders and Recursive Path Orders
• KBO orientability
• Things to know when implementing KBO
• Tyrolean termination tool: techniques and features

Describes a project that uses

Uses Software

• REVE

This page was built for publication: Automating the Knuth Bendix ordering

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q751830)