Automated reasoning is an established field with a long history and many ideas. E-graph rewriting techniques fits into this history. This connection suggests roads to implementing fundamental extensions to e-graph rewriting.
- Union Finds are Atomic Ground Completion
- E-Graphs are Ground Completion
- Ground Superposition is a contextual E-graph
- Lambda superposition holds clues / is a lambda e-graph
- Completion is an E-Graph with unification variables / first class rules
Twee, Vampire, E-prover, and Zipperposition are capable of doing the same thing as egg if they supported the right interfaces.
- Abstract https://github.com/philzook58/egraphs2024-talk/blob/main/egraphs2024_abstract.pdf
- Talk notebook https://github.com/philzook58/egraphs2024-talk/blob/main/egraphs_talk.ipynb
Presented at PLDI EGRAPHS 2024 https://pldi24.sigplan.org/details/egraphs-2024-papers/13/E-graphs-and-Automated-Reasoning-Looking-back-to-look-forward