Vegie

Title

Proof Primitives for Equality Saturation-based Automated Provers

Publication

VeriLang 2026, co-located with ECOOP 2026 in Brussels.

• VeriLang 2026: Proof Primitives for Equality Saturation-based Automated Provers
• Preprint: PDF
• Code: github.com/gzakhour/vegie

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.