Vampire's Home Page


(A few days in the future) Version 3.0 of Vampire used at CASC-24 is available and can be downloaded.
(June 2013) Vampire is winning CASC yet again! Vampire has won the world cup in theorem proving CASC held at 24th International Conference on Automated Deduction (CADE). This time Vampire was the winner in the main division of the competition FOF (first-order formulas). All together Vampire won 28 division titles in CASC since 1999: more than any other theorem prover in the history of the competition. Vampire won all the FOF divisions since 2002.


Automatic theorem proving has a number of important applications, such as Software Verification, Hardware Verification, Hardware Design, Knowledge Representation and Reasoning, Semantic Web, Algebra and Proving Theorems in Mathematics. Over 50 years of research in theorem proving have resulted in one of the most advanced and elegant theories in computer science. This area is an ideal target for scientific engineering: implementation techniques have to be developed to realise an advanced theory in practically valuable tools.

Vampire is a theorem prover, that is, a system able to prove theorems. More precisely, it proves theorems in first-order logic. The development of Vampire has begun in 1994. The current version belongs to the third generation of Vampire, see the authors information for details.

Vampire is very fast, as can be judged by our awards.