Andrei Voronkov's Homepage
News
(January 2012) Ten Turing Award Winners, Garry Kasparov and other outstanding scientists
will speak at the Turing Centenary Conference!
(July 2011) Vampire is winning CASC, this time in two divisions! Vampire has won two divisions of the world cup in theorem
proving CASC held at 23rd International Conference on Automated
Deduction (CADE). It has won the main division of the competition FOF
(first-order formulas) and the LTB division
(very large problems, coming from ontologies).
in conjunctive normal form) and the LTB division
(very large problems, coming from ontologies). In both
divisions Vampire solved more problems than all other
systems together. In the FOF division
Vampire solved 269 problems versus 265 problems solved by
all other systems.
In the LTB division
Vampire solved 139 problems versus 122 problems solved by
all other systems.
All together
Vampire has won 25 division titles in CASC since 1999:
more than any other theorem prover. Vampire also came second in the
CNF division (formulas in conjunctive normal form) and EPR division
(effectively propositional formulas).