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)

zbMATH Keywords

completion algorithmKnuth-Bendix ordering

Mathematics Subject Classification ID

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

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

• 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?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• 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

(20)

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

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)