Automated Theorem Proving Competition Success (CASC-22)

Congratulations to Andrei Voronkov and Krystof Hoder with Vampire and Konstantin Korovin with iProver. Both provers have won major divisions yet again at the annual World Cup in Theorem Proving (CASC) which was held at the 22nd International Conference on Automated Deduction (CADE-22), whose programme chair was Renate Schmidt.

 

Manchester systems Vampire and iProver, won 4 divisions out of 7:

Vampire won:

• FOF - arbitrary problems (the main division). This is the 8th successive year that Vampire has won the FOF division.
• CNF - formulas in conjunctive normal form. The 9th successive year that Vampire has won the CNF division.
• LTB - very large theories.

 

iProver won:

• EPR - formulas with no function symbols. This is the 2nd successive year Konstantin's iProver has won the EPR division.