The design of the CADE-13 ATP System Competition

Christian Suttner; Geoff Sutcliffe

doi:10.1023/A:1005802523220

The design of the CADE-13 ATP System Competition

Christian Suttner, Geoff Sutcliffe

Research output: Contribution to journal › Article › peer-review

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 language	English (US)
Pages (from-to)	139-162
Number of pages	24
Journal	Journal of Automated Reasoning
Volume	18
Issue number	2
DOIs	https://doi.org/10.1023/A:1005802523220
State	Published - Jan 1 1997
Externally published	Yes

Keywords

Automated theorem proving
Competition
Design

ASJC Scopus subject areas

Software
Computational Theory and Mathematics
Artificial Intelligence

Access to Document

10.1023/A:1005802523220

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

Cite this

@article{a5a04b2b34114263bd47df68ae9df70c,

title = "The design of the CADE-13 ATP System Competition",

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.",

keywords = "Automated theorem proving, Competition, Design",

author = "Christian Suttner and Geoff Sutcliffe",

year = "1997",

month = jan,

day = "1",

doi = "10.1023/A:1005802523220",

language = "English (US)",

volume = "18",

pages = "139--162",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "2",

}

TY - JOUR

T1 - The design of the CADE-13 ATP System Competition

AU - Suttner, Christian

AU - Sutcliffe, Geoff

PY - 1997/1/1

Y1 - 1997/1/1

N2 - 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.

AB - 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.

KW - Automated theorem proving

KW - Competition

KW - Design

UR - http://www.scopus.com/inward/record.url?scp=0031108580&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031108580&partnerID=8YFLogxK

U2 - 10.1023/A:1005802523220

DO - 10.1023/A:1005802523220

M3 - Article

AN - SCOPUS:0031108580

VL - 18

SP - 139

EP - 162

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 2

ER -