Dis/Equality Graphs

This conference talk from POPL 2025 presents groundbreaking research on Dis/Equality Graphs by researchers from the University of St. Gallen. Explore how this work extends e-graphs—data structures used to represent program spaces and reason about term equality—by adding direct support for disequalities. Learn about the first formal proof demonstrating the equivalence of e-graphs to the reflexive, symmetric, transitive, and congruent closure of their encoded equivalence relation. Discover the analytical and empirical evidence showing that direct disequality support outperforms traditional equality embedding techniques used in SMT solvers and automated verifiers. The presentation covers the implementation of this approach as an extension to egg (a popular Rust e-graph library) and evaluates its performance in SMT solving and automated theorem proving contexts. The research includes reusable artifacts available through Zenodo, making it valuable for those working in program optimization, automated reasoning, and formal verification.