Formalizing Knuth-Bendix orders and Knuth-Bendix completion
From MaRDI portal
Recommendations
Cited in
(16)- Formalization of the resolution calculus for first-order logic
- A Knuth-Bendix-like ordering for orienting combinator equations
- Certified equational reasoning via ordered completion
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- Knuth-Bendix completion for non-symmetric transitive relations
- Certified Kruskal's tree theorem
- Certifying confluence proofs via relative termination and rule labeling
- A Mechanized Proof of Higman’s Lemma by Open Induction
- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
- scientific article; zbMATH DE number 7204438 (Why is no real title available?)
- Abstract completion, formalized
- Order Reconfiguration under Width Constraints
- Left-Linear Completion with AC Axioms
- Weighted Path Orders Are Semantic Path Orders
- Certifying the weighted path order (invited talk)
- Left-linear completion with AC axioms
Describes a project that uses
Uses Software
This page was built for publication: Formalizing Knuth-Bendix orders and Knuth-Bendix completion
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2958390)
