Augmenting Rewrite Rule Sets via Knuth-Bendix Completion
summary
Pipeline runs Knuth-Bendix completion (via a tree equational theorem prover) to generate extra oriented rewrite rules, stops after N ≈ 100-rule sweet spot, then feeds the augmented set to an e-graph-based equality saturation engine. Empirical results: KBC-augmented sets reach slightly better reductions (13→14 symbols) and hit similar quality roughly 10x speedup at small budgets; greedy rewriting remains worse. Handles group axioms (inventing double-inverse rules) but struggles with unorientable/commutativity rules. Tools: Knuth-Bendix completion + e-graph.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:55Rule set optimization
- 3:24Rule application approaches
- 5:31Knuth-Bendix completion
- 9:27Termination guarantees
- 10:34Knuth-Bendix with E-graphs
- 12:01Algorithm design
- 14:06Runtime results
- 16:13Greedy rule evaluation
- 18:46Ongoing work
- 19:51Future directions
- 20:13Conclusion and key takeaways
- 20:59Q&A
related talks
14mRewrite Rule Inference Using Equality Saturation
29mSemantic Transformation Framework for Rewriting Rules
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
15mValidating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…)
38mE-graphs and Automated Reasoning: Looking back to look forward
29mType Checking with Rewriting Rules
19mDestructive E-Graph Rewrites
21mChecking Equivalence in a Non-strict Language