Andrei Voronkov's Homepage

(February 2008) LPAR 2008 will be held in Qatar. LPAR 2008 programme chairs will be Iliano Cervesato, Helmut Veith and myself.

(July 2007) Vampire is winning CASC in two divisions again. Vampire has won two divisions of the world cup in theorem proving CASC held at 21st International Conference on Automated Deduction (CADE). It has won the main division of the competition FOF (first-order formulas) and the CNF division (formulas in conjunctive normal form.) In the CNF division Vampire solved 182 problems out of 200 while all other systems taken together solved 174 problems. All together Vampire has won 15 division titles in CASC since 1999: more than any other theorem prover.