The recent work on relational, datalog-inspired egraphs in PLDI this year ("Unifying Datalog and Equality Saturation") is actually interesting because it can so

The recent work on relational, datalog-inspired egraphs in PLDI this year ("Unifying Datalog and Equality Saturation") is actually interesting because it can solve cases like the y/x*x -> y identity example, by the power of an interval analysis on x (among other things.) Sort of like adding a postulate to a rewrite term and then proving it. But instead it's by adding relations between terms in the graph. See section 6.2 of the paper. https://github.com/egraphs-good/egglog https://github.com/egraphs-good/egglog https://arxiv.org/pdf/2304.04332.pdf https://arxiv.org/pdf/2304.04332.pdf