Vampire is an automatic theorem prover for first-order classical logic developed in the Department of Computer Science at the University of Manchester.

Since Version 4, the development has involved a wider international team including Laura Kovacs, Giles Reger, and Martin Suda.

A number of standard redundancy criteria and simplification techniques are used for pruning the search space: tautology deletion, subsumption resolution, rewriting by ordered unit equalities, basicness restrictions and irreducibility of substitution terms.

When a theorem is proven, the system produces a verifiable proof, which validates both the clausification phase and the refutation of the conjunctive normal form.

[5] As of November 2020, Vampire is released under a modified version of the BSD 3-clause licence that explicitly permits commercial use.