The CADE-25 ATP System Competition CASC-25

摘要

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. One purpose of CASC is to provide a public evaluation of the relative capabilities of ATP systems. Additionally, CASC aims to stimulate ATP research, motivate development and implementation of robust ATP systems that are useful and easily deployed in applications, provide an inspiring environment for personal interaction between ATP researchers, and expose ATP systems within and beyond the ATP community. Fulfillment of these objectives provides insight and stimulus for the development of more powerful ATP systems, leading to increased and more effective use. CASC-25 was held on 4th August 2015 as part of the 25th International Conference on Automated Deduction (CADE-25), run on computers supplied by the StarExec project. CASC is run in divisions according to problem and system characteristics. For CASC-25 the divisions were: 1. THF: Typed Higher-order Form theorems (axioms with a provable conjecture). 2. THN: Typed Higher-order form Non-theorems (axioms with a countersatisfiable conjecture, and satisfiable axiom sets). This division was new for CASC-25. 3. TFA: Typed First-order with Arithmetic theorems (axioms with a provable conjecture). 4. TFN: Typed First-order with arithmetic Non-theorems (axioms with a countersatisfiable conjecture, and satisfiable axiom sets). This division was new for CASC-25. 5. FOF: First-Order Form theorems (axioms with a provable conjecture). 6. FNT: First-order form syntactically non-propositional Non-Theorems (axioms with a countersatisfiable conjecture, and satisfiable axiom sets). 7. EPR: Effectively PRopositional clause normal form (non-)theorems. 8. LTB: First-order form theorems (axioms with a provable conjecture) from Large Theories, presented in Batches with a shared time limit. Problems for CASC are taken from the TPTP Problem Library. The TPTP version used for CASC is released after the competition, so that new problems have not been seen by the entrants. The THF, TFA, FOF, FNT, and LTB divisions were ranked according to the number of problems solved with an acceptable proof/model output. The THN, TFN, and EPR divisions were ranked according to the number of problems solved, but not necessarily accompanied by a proof or model. Ties are broken according to the average time over problems solved. Division winners are announced and prizes are awarded.