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:

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:

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:

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.