Versioned E-Graphs (and more!)
Speaker: Jahrim Gabriele Cesario and George Zakhour2026-10-15
E-graphs were first introduced as a data structure for equational reasoning in theorem provers. Yet proofs often require reasoning beyond plain equalities, such as disequalities or conditional equalities, where e-graph support is still developing.
In this talk, we present Versioned E-Graphs for conditional reasoning. Versioned e-graphs efficiently encode multiple equivalence relations (versions) in a single structure by sharing e-nodes and equalities across versions. We discuss the challenges they raise, such as termination, and how these shape our algorithms.
We then demonstrate their applicability through proof production in our prototype inductive prover Vegie.
We conclude with future extensions that can benefit the theorem-proving ecosystem, such as richer relations between versions and parallelism, developed as part of our Smart E-Graphs project. ```