| Features | Vampire's Home PageNews(October 26, 2009) Vampire is now available. The new version of Vampire is available and can be downloaded. (August 5, 2009) Vampire has won CASC again. Vampire has won the world cup in theorem proving CASC held at the 22nd International Conference on Automated
Deduction (CADE-22),
this time in three divisions. It has won the main division of the competition FOF
(first-order formulas), the CNF division (formulas
in conjunctive normal form) and the LTB division
(the large theories division). In the CNF division
Vampire solved 181 problems out of 200 while all other
systems taken together solved 174 problems. All together
Vampire has won 20 division titles in CASC since 1999:
more than any other theorem prover. VampireAutomatic 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. |