Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Michael Rawson, Andrei Voronkov, Johannes Schoisswohl, Anja Petković Komel · Lecture notes in computer science · 2025
Abstract The Vampire automated theorem prover is extended to output proofs in such a way that each inference is represented by a quantifier-free SMT instance. If every instance is unsatisfiable, the proof can be considered verified by an external SMT solver. This pragmatic form of proof checking places only a very light burden on the SMT solver, and can easily handle inferences that other systems may find difficult, such as theory inferences or extensive ground reasoning. The method is considerably easier to implement than proof formats based on small kernels and covers a greater variety of modern-day inferences.