The design of the CADE-13 ATP System Competition

Christian Suttner, Geoff Sutcliffe

Research output: Contribution to journalArticlepeer-review

12 Scopus citations


Running a competition for automated theorem proving (ATP) systems is a difficult and arguable venture. However, the potential benefits of such an event by far outweigh the controversial aspects. The motivations for running the CADE-13 ATP System Competition were to contribute to the evaluation of ATP systems, to stimulate ATP research and system development, and to expose ATP systems to researchers both within and outside the ATP community. This article identifies and discusses the issues that determine the nature of such a competition. Choices and motivated decisions for the CADE-13 competition, with respect to the issues, are given.

Original languageEnglish (US)
Pages (from-to)139-162
Number of pages24
JournalJournal of Automated Reasoning
Issue number2
StatePublished - 1997
Externally publishedYes


  • Automated theorem proving
  • Competition
  • Design

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


Dive into the research topics of 'The design of the CADE-13 ATP System Competition'. Together they form a unique fingerprint.

Cite this