Note IV Independent explainer
The CASC theorem prover competition, explained
Every year automated theorem provers are put on identical problems under a strict clock. This is how the competition is organised and how to read its results.
What CASC is
CASC is the CADE ATP System Competition. CADE is the Conference on Automated Deduction, and the competition runs as part of that conference or of the joint conference IJCAR when the two meet. It was first held in 1996, and its purpose is to evaluate fully automatic provers for classical logic and to encourage their development.
How a round works
Entrants are complete systems that run without any human help. Each system is given problems written in the TPTP format and has to print an answer in the SZS style within a fixed wall-clock time limit per problem. All systems run on the same kind of hardware, so the comparison is about software rather than budget.
Problems are chosen from the TPTP library, and the organisers take care that a problem was not simply known and tuned for in advance, for example by drawing at random from a large pool and by including problems unseen by the entrants.
Divisions
The competition is split into divisions by problem class and logic. Examples are first-order formulas, clause normal form problems, problems that consist only of equations, typed arithmetic problems and higher-order problems. A system can enter several divisions, and each division has its own ranking. The official rules of each year define exactly how answers are scored.
How a winner is chosen
In the main divisions the system that solves the most problems wins, with ties broken by total time. Because the problems are hard and a time limit applies, the numbers separate systems clearly, yet a different set of problems or a different limit could change the order.
What the results tell you
CASC is a useful snapshot of what general-purpose provers can do today and a driver for progress, because authors compare strategies and implementation ideas each year. It does not show which prover is best for a particular research problem. A prover that is fast on competition-style problems can lose on a large industrial one, and the reverse is also true.
To follow the current results, read the official competition pages, which list entrants, rules and rankings for each year.