History and Authors

Vampire had several predecessors implemented by Andrei Voronkov in the International Laboratory of Intelligent Systems in Novosibirsk from 1990. The first predecessor that was actually able to prove something appeared in 1989 and called Drakosha. It has been implemented in LISP.

There have been three major incarnations of Vampire itself, all implemented in C++.

The first incarnation was born in Uppsala University in 1994 after Andrei Voronkov's visit to the Bull Research Lab. This implementation was used for the first experiments with code trees and a pre-CASC competition with the SETHEO theorem prover in Munich.
The second re-incarnation appeared in Uppsala University and then wandered to the University of Manchester. It has been developed from the first incarnation (that was eventually completely rewritten) by Andrei Voronkov and Alexandre Riazanov in 1998. From 2005 it has been developed and maintained by Andrei Voronkov. This incarnation was winning the CASC competitions since 1999.
The work on third re-incarnation of Vampire started in 2008. It has been developed by Andrei Voronkov and Krystof Hoder. This version used some code and algorithms for preprocessing from the second re-incarnation but re-implemented the resolution and superposition engine from scratch. The version used in CASC 2009 was actually a combination of the second and the third reincarnations glued by Perl scripts called Dracula and Drakosha.
Since Krystof Hoder decided to leave academia and help Larry Page and Sergey Brin to make more money, Vampire is waking up for its fourth reincarnation. Several people are working on it. A considerable amount of code was contributed by Laura Kovacs, mainly in Vampire's program analysis, interpolation and symbol elimination parts. Ioan Drăgan is now implementing the program analysis part and theories.