In order to stimulate ATP system development and to expose ATP systems to interested researchers, an ATP competition will be held at CADE-13. The competition will evaluate the performance of sound fully automatic ATP systems, on first-order CNF theorems chosen from the TPTP Problem Library. The evaluation will be in terms of the number of theorems proved, and the time taken; in the context of a specified time limit for each proof attempt, and a bounded number of eligible TPTP theorems. Click here for an overview of the competition and the rules, and also for the competition technical report giving full details. Enquiries can be sent to the competition organizers.

ARPA-owned and maintained machines will be provided for the competition by the Center for Computer Aids for Industrial Productivity, Rutgers University.

Organizing Committee: Christian Suttner (TU München, Germany) suttner@informatik.tu-muenchen.de; Geoff Sutcliffe (James Cook University, Australia) geoff@cs.jcu.edu.au.

The competition schedule is below. A continuous overview of current results will be displayed while the competition is in progress. System demonstrations will also be possible while the competition is in progress.

Meeting of Competitors: 10:30.
Competition in Progress: 10:45-12:15.
Lunch Break: 12:15-14:00.
Competition in Progress: 14:00-17:00.
Announcement of Competition Results by Competition Panel: 17:35.