The CADE ATP System Competition -- CASC

The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic automated theorem-proving (ATP) systems for classical logic -- the world championship for such systems. CASC provides a public evaluation of the relative capabilities of ATP systems, and aims to stimulate ATP research toward the development of more powerful ATP systems. Over the years CASC has been a catalyst for impressive improvements in ATP. CASC is held at the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR, which replaces CADE on alternate years) each year. These conferences are the major forums for the presentation of new research in all aspects of automated deduction. The evaluation is in terms of the number of problems solved, the number of solutions output, and the average run time for problems solved in the context of a bounded number of eligible problems, chosen from the TPTP Problem Library (Sutcliffe 2009), and a CPU time limit for each solution attempt. One purpose of CASC is to provide a public evaluation of the relative capabilities of ATP systems.