Slothrop: Knuth-Bendix Completion with a Modern Termination Checker

DOI10.1007/11805618_22MaRDI QIDQ3527302zbMATH OpenOpenAlexFDO

Authors Ian Wehrman, Aaron Stump, Edwin Westbrook

Publication date 25 September 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
• Completion procedures as semidecision procedures
• Multi-completion with Termination Tools (System Description)
• Formalizing Knuth-Bendix orders and Knuth-Bendix completion
• scientific article; zbMATH DE number 4076598

Cited in

(17)

• Termination tools in ordered completion
• AC completion with termination tools
• A lower bound of the number of rewrite rules obtained by homological methods
• Left-linear completion with AC axioms
• Completion and reduction orders (invited talk)
• Towards automated deduction in cP systems
• Multi-completion with Termination Tools (System Description)
• Slothrop
• Order Reconfiguration under Width Constraints
• Formalizing Knuth-Bendix orders and Knuth-Bendix completion
• Encoding dependency pair techniques and control strategies for maximal completion
• Multi-completion with termination tools
• Paramodulation with non-monotonic orderings and simplification
• Left-Linear Completion with AC Axioms
• Completion for logically constrained rewriting
• KBCV – Knuth-Bendix Completion Visualizer
• Completion after program inversion of injective functions

Describes a project that uses

Uses Software

• CiME
• AProVE
• OCaml

This page was built for publication: Slothrop: Knuth-Bendix Completion with a Modern Termination Checker

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