Abstract
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/