Theorem Proving and Vampire
Theorem Proving
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
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
Our tropheys
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.
When will the next version of Vampire be available?
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.