Automatic theorem proving has a number of important applications, such as Verification of Software and Hardware, Hardware Design, Knowledge Representation and Proving Theorems in Mathematics.

Over 30 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. You can read the following publications on Vampire to learn more about it:

- A. Voronkov. The Anatomy of Vampire: Implementing Bottom-Up Procedures with Code Trees Journal of Automated Reasoning v. 15 (2), 1995, 237-265
- A. Riazanov, A. Voronkov. Partially Adaptive Code Trees. JELIA 2000, LNCS v. 1919, Springer Verlag 2000, pp. 209-223.
- A. Riazanov, A. Voronkov. The Design and Implementation of {Vampire}}, AI Communications, v 15(2-3), 2002, pp. 91-110.
- R. Nieuwenhuis, T. Hillenbrand, A. Riazanov, A. Voronkov. On the Evaluation of Indexing Techniques for Theorem Proving. IJCAR 2001, LNCS v. 2083, Springer Verlag 2001, pp. 257-271.
- A. Voronkov. Algorithms, Datastructures, and Other Issues in Efficient Automated Deduction. IJCAR 2001, LNCS v. 2083, Springer Verlag 2001, pp. 13-28.
- A. Riazanov, A. Voronkov. Splitting without backtracking. IJCAI 2001, v. 1, 2001, pp. 611-617.
- A. Riazanov, A. Voronkov. Limited Resource Strategy in Resolution Theorem Proving. Journal of Symbolic Computation, v 36 (1-2), 2003, pp. 101-115.
- D. Tsarkov, A. Riazanov, S. Bechhofer, I. Horrocks. Using Vampire to Reason with OWL. ISWC 2004, LNCS v. 3298, Springer Verlag, 2004, pp. 471-485
- A. Riazanov, A. Voronkov. Efficient Checking of Term Ordering Constraints. IJCAR 2004, LNCS v. 3097, Springer Verlag v. 3097, pp. 60-74.
- U. Hustadt, B. Konev, A. Riazanov, A. Voronkov. TeMP: A Temporal Monodic Prover. IJCAR 2004, LNCS v. 3097, Springer Verlag v. 3097, pp. 326-330.
- A. Riazanov, A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, v. 199 (1-2), 2005, pp. 228-252.
- I. Horrocks, A. Voronkov Reasoning Support for Expressive Ontology Languages Using a Theorem Prover. FoIKS 2006, LNCS v. 3861, Springer Verlag, 2006, pp. 201-218

Vampire is winning at least one division of the world cup in theorem proving CASC since 1999. All together Vampire won 17 titles: more than any other prover. We traditionally take part in the following two divisions of the competition:

- The FOF division: unrestricted first-order problems. This division was ranked second in importance after the MIX division before 2007 and is now recognised as the main competition division.
- The CNF division: first-order problems in conjunctive normal form. This division was called MIX before 2007 and recognised as the main competition division.

We also participate in other, more special competition divisions but Vampire is not specialised for them so our achievements are mostly modest.

Here is the list of our achievements:

**2008:**winner in both FOF and CNF divisions. In the CNF division Vampire solves more problems than all other provers together.**2007:**winner in both FOF and CNF divisions. In the CNF division Vampire solves more problems than all other provers together.**2006:**winner in both MIX and FOF divisions. In the CNF division Vampire solves more problems than all other provers together.**2005:**winner in both MIX and FOF divisions. In the MIX division Vampire solves more problems than all other provers together.**2004:**winner in both MIX and FOF divisions. In the FOF division Vampire solves more problems than all other provers together.**2003:**winner in both MIX and FOF divisions.**2002:**winner in both MIX and FOF divisions.**2001:**winner in the MIX division.**2000:**winner in the FOF division.**2001:**winner in the MIX division.

We are working on building a completely new version of Vampire that we believe will be more advanced and faster than the previous ones. It is difficult to say when exactly it will be available but the end of 2008 is a good guess. Note that we do not maintain the old version any more.