EGRAPHS Community

Equality reasoning in Vampire

Video

2026-02-19

Marton Hajdu from the Vampire team will present his work on equality reasoning in the Vampire tool.

Abstract

Reasoning in first-order logic with equality is challenging due to the combination of quantifiers and equality axioms that often results in proof search space explosion. In this talk, we present how modern theorem provers, like Vampire, handle this explosion using the state-of-the-art superposition calculus, which is based on the concept of redundancy. We then examine one of the most useful redundancy elimination techniques, called demodulation (also called simplification with unit equalities), and its inner workings in Vampire. Doing so, we look at two specialized data structures in the context of first-order theorem proving, called code trees and term ordering diagrams, that also contributed to the recent successes of Vampire at the World Championship for Automated Theorem Proving (CASC), winning all trophies for the first time in the history of CASC.

Bio:

Márton Hajdu joined the Vampire team at TU Wien in 2021 as a PhD student, under supervision of Laura Kovács and co-supervision of Andrei Voronkov (University of Manchester). During his PhD, he worked first on inductive reasoning, later on improving core data structures and first-order reasoning with equality in Vampire. He currently works full-time as a Research Software Engineer at TU Wien.