Orienting rewrite rules with the Knuth-Bendix order.

DOI10.1016/S0890-5401(03)00021-XMaRDI QIDQ1401932zbMATH OpenFDO

Authors Konstantin Korovin, Andrei Voronkov

Publication date 19 August 2003

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

Full work available at URL https://doi.org/10.1016/S0890-5401(03)00021-X

zbMATH Keywords

Knuth-Bendix ordersOrdering constraintsOrientabilityTerm rewritingTermination

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 1722704
• KBO orientability
• Automated Deduction – CADE-20
• Satisfying KBO Constraints
• Automating the Knuth Bendix ordering

Cites work

• Automating the Knuth Bendix ordering
• Handbook of automated reasoning. In 2 vols
• scientific article; zbMATH DE number 3870642 (Why is no real title available?)
• scientific article; zbMATH DE number 3921958 (Why is no real title available?)
• scientific article; zbMATH DE number 4041334 (Why is no real title available?)
• scientific article; zbMATH DE number 176755 (Why is no real title available?)
• scientific article; zbMATH DE number 1234104 (Why is no real title available?)
• scientific article; zbMATH DE number 1342225 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• scientific article; zbMATH DE number 1754649 (Why is no real title available?)
• scientific article; zbMATH DE number 1456949 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Invariants, patterns and weights for ordering terms
• On recursive path ordering
• Simple LPO constraint solving methods
• SOLVING SYMBOLIC ORDERING CONSTRAINTS

Cited in

(17)

• The size-change principle and dependency pairs for termination of term rewriting
• scientific article; zbMATH DE number 1722704 (Why is no real title available?)
• AC-KBO revisited
• αCheck: A mechanized metatheory model checker
• Transforming SAT into termination of rewriting
• On transfinite Knuth-Bendix orders
• Automated Deduction – CADE-20
• Satisfying KBO Constraints
• Completeness and Herbrand theorems for nominal logic
• Towards automated deduction in cP systems
• KBO Constraint Solving Revisited
• Term ordering diagrams
• Linear termination is undecidable
• Automating the Knuth Bendix ordering
• KBO orientability
• Things to know when implementing KBO
• Tyrolean termination tool: techniques and features

This page was built for publication: Orienting rewrite rules with the Knuth-Bendix order.

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