EGraphs and Automated Reasoning: Looking Back to Look Forward

EGraphs can be seen as an instance of ground completion and this lends ideas to how to extend them with lambdas, context, and destructive rewriting.
- Abstract github.com/philzook58/egraphs...
- Blog posts:
+ www.philipzucker.com/egraph-g...
+ www.philipzucker.com/ground-r...
+ www.philipzucker.com/bottom_up/
- References
+ Term Rewriting and All That (TRAAT)
+ Handbook of Automated Reasoning
+ Automated Reasoning: Introduction and Applications
Also given at EGRAPHS 2024.