Disequality Reasoning
E-graphs that natively know when two terms must differ. Refutation becomes a first-class operation instead of an encoding trick, with a simpler metatheory and better performance than the embeddings used in SMT solvers.
Equality is Just The Beginning:Semantic-Aware E-Graphs
E-graphs store bare equalities: they do not know why an equality holds, when it applies, or how it relates to other facts, so tools compensate with costly workarounds. We push that semantic knowledge into the data structure itself, proving faster.
Semantic Extensions
Conditional Reasoning
Equalities rarely hold unconditionally. Versioned e-graphs encode a whole family of equivalence relations at once, one per set of assumptions, so proof branches can avoid replicating facts they agree on.
Lazy Reasoning
Equivalence relations form a lattice. Lazy meet and join operations compose the knowledge of independently explored contexts on demand, touching only the equalities a query actually needs.
In progress
Parallel Reasoning
The lattice structure exposes which reasoning tasks are independent. Scheduling proof exploration as parallel tasks over a lattice of e-graphs turns semantic awareness into raw speed.
In progress
Publications
Proof Primitives for Equality Saturation-based Automated Provers
VeriLang 2026, ECOOP, July 2026
Abstract
We present a proof extraction algorithm for versioned e-graphs, an extension of e-graphs that supports branching reasoning contexts and proof by cases. In the setting of algebraic datatypes, the algorithm handles rewrites, congruence, injectivity, contradictions, induction, and case splits. We implement it in Vegie, a lightweight automated inductive theorem prover. An early case study suggests that the produced proofs are smaller than those of a state-of-the-art e-graph prover.
Versioned E-Graphs
Proc. ACM Program. Lang. 10, PLDI, Article 171, June 2026
Abstract
E-graphs are an efficient encoding for discovering and maintaining sets of equalities. In several scenarios, equalities may hold only conditionally, i.e., under certain assumptions: in automated provers the proof is often split into multiple branches, each considering a different set of equalities. Traditional e-graphs can only encode a single set of equalities at a time, so conditional equalities are handled by maintaining multiple e-graphs, replicating the equalities shared among branches. Versioned e-graphs efficiently encode multiple equivalence sets at the same time, maximizing shared information among them. Compared to widely-adopted solutions that maintain multiple e-graphs, versioned e-graphs are up to 5–30% more memory efficient and up to 4× faster, especially when solution spaces are large both in explored program terms and number of branches.
Dis/Equality Graphs
Proc. ACM Program. Lang. 9, POPL, Article 77, January 2025
Abstract
In many applications it is necessary to reason about disequality of terms as well as equality. While disequality reasoning can be encoded, direct support for disequalities increases performance and simplifies the metatheory. This paper develops an implementation-independent framework to formally reason about e-graphs, proving for the first time the equivalence of e-graphs to the closure of the equivalence relation they encode. It presents the first formalization of an e-graph extension that directly supports disequalities, with an analytical result about their superior efficiency compared to common embedding techniques. The approach is implemented as an extension to egg and evaluated in an SMT solver and an automated theorem prover, where direct support for disequalities outperforms encodings based on equality embedding.
Credits
