The design of the CADE-13 ATP System Competition

Christian Suttner, Geoff Sutcliffe

Research output: Contribution to journalArticle

11 Scopus citations

Abstract

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
Volume18
Issue number2
DOIs
StatePublished - Jan 1 1997
Externally publishedYes

Keywords

  • Automated theorem proving
  • Competition
  • Design

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

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

  • Cite this