The Vampire Diary

Abstract

During the past years of continuous development, the Vampire theorem prover has become an automated solver for machine-based proof search in the combined theories of commonly-used data structures. Central to Vampire is saturation-based first-order theorem proving using the superposition calculus, which has by now extended to support arithmetic, induction, code synthesis, higher-order logic, proof certification, and many more. These advances have been made to meet the demands of mathematical formalization and trustworthy system development. In this talk we discuss the aforementioned advances in Vampire, overview the main changes Vampire has undergone during the past years, and survey some of the design choices we made during this process. We believe our advances in saturation-based reasoning proved to make a difference. Vampire outperforms or complements many other state-of-the-art reasoners, including leading SMT solvers and inductive theorem provers. For example, in the past two editions of the CASC world championship in theorem proving, Vampire won all competition divisions and proved more problems than any other system in every competition division. This talk is based on the joint work of the Vampire developers’ team, including Filip Bártek, Ahmed Bhayat, Jonas Bodingbauer, Robin Coutelier, Bernhard Gleiss, Márton Hajdu, Matthias Hetzenberger, Petra Hozzová, Jack McKeown, Merisa Mustajbasic, Jakob Rath, Michael Rawson, Axel Polaczek, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov, and Eva-Maria Wagner. Our work was funded in whole or in part by the ERC Consolidator Grant ARTIST 101002685, the ERC Proof of Concept Grant LEARN 101213411, the FWF SpyCoDe Grant 10.55776/F85, the SBA Research COMET Center SBA-K1 NGC managed by the FFG, and the WWTF grant [ForSmart Grant ID: 10.47379/ICT22007].