The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic, first-order Automated Theorem Proving (ATP) systems - the world championship for such systems. In addition to the primary aim of evaluating the relative capabilities of ATP systems, CASC aims to stimulate ATP research in general, to stimulate ATP research towards autonomous systems, to motivate implementation and fixing of systems, to provide an inspiring environment for personal interaction between ATP researchers, and to expose ATP systems within and beyond the ATP community. Fulfillment of these objectives provides stimulus and insight for the development of more powerful ATP systems, leading to increased and more effective usage. CASC-J4 was held on 13th August 2008, as part of the 4th International Joint Conference on Automated Reasoning, in Sydney, Australia. It was the thirteenth competition in the CASC series (lucky for some). The CASC-J4 web site provides access to details of the competition design, competition resources, and the systems that were entered: http://www.tptp.org/CASC/J4/ CASC-J4 was (like all CASCs) divided into divisions according to problem and system characteristics. There were competition divisions in which systems were explicitly ranked, and a demonstration division in which systems could demonstrate their abilities without being formally ranked. For analysis purposes, the divisions were additionally split into categories according to the syntactic characteristics of the problems. The competition divisions were (see the web site for details): (1) FOF -^sFirst-order form theorems (axioms with a provable conjecture) (2) FNT -^sFOF non-theorems (axioms with a counter-satisfiable conjecture, and satisfiable axiom sets) (3) CNF -^sClause normal form theorems (unsatisfiable clause sets) (4) SAT -^sCNF non-theorems (satisfiable clause sets) (5) EPR -^sCNF effectively propositional theorems and non-theorems (6) UEQ -^sUnit equality CNF theorems (7) LTB -^sFOF problems from large theories, presented in batches.
展开▼
