First-Order Theorem Proving and Vampire

In this paper we give a short introduction in first-order theorem provingand the use of the theorem prover VAMPIRE. We discuss the superpositioncalculus and explain the key concepts of saturation and redundancy elimination,present saturation algorithms and preprocessing, and demonstrate how these concepts are implemented in VAMPIRE. Further, we also cover more recent topics and features of VAMPIRE designed for advanced applications, including satisfiability checking, theory reasoning, interpolation, consequence elimination, and program analysis