E-graphs and Automated Reasoning: Looking back to look forward
summary
Argues that e-graphs are essentially an instance of ground completion = e-graph rewriting, demonstrates a Python tool that inverts the completion/tree diagram and recovers directed rewrite edges lost by standard e-graphs, and shows how flattening terms with fresh constants makes term orders correspond to extraction objectives. Connects this to tree automata, contrasts top‑down vs bottom‑up matching, and sketches paths toward contextual/lambda support and principled destructive rewriting using ideas from zipperposition and vampire.
AI-written summary · about
chapters (8)
- 0:00E-graphs introduction
- 6:13Greedy simplification vs e-graphs
- 10:27Equational completion benefits
- 18:11Confluence and union-find
- 23:22Visualizing e-graphs
- 27:15E-matching and automata
- 30:07Contexts and destructive rewriting
- 34:02Future directions
related talks
22mFrom Rewriting to Fixpoints: Solving Recursive Equations with E-Graphs
23mE-graphs modulo theories
14mPredicate E-Graphs with Symbolic Conditional Rewriting
19mDestructive E-Graph Rewrites
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
25mLifting E-Graphs: A Function Isn’t a Constant
23mVersioned E-Graphs
32mExperience Report: Graph Rewriting with Lexical Effect Handlers