Small Proofs from Congruence Closure - FMCAD 2022

E-graphs (or congruence closure) are a key data structure in solvers for optimization or synthesis of programs. In this talk, we show a new algorithm for finding smaller proofs from e-graphs.