The design of the CADE-13 ATP system competition

Christian B. Suttner; Geoff Sutcliffe

doi:10.1007/3-540-61511-3_76

The design of the CADE-13 ATP system competition

Christian B. Suttner, Geoff Sutcliffe

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

3 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 are to contribute to the evaluation of ATP systems, to stimulate ATP research and system development, and to expose ATP systems to interested researchers both within and outside the ATP community. This paper identifies and discusses the issues that determine the nature of the competition. Choices and motivated decisions, with respect to the issues, are given.

Original language	English (US)
Title of host publication	Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings
Editors	John K. Slaney, Michael A. McRobbie
Publisher	Springer Verlag
Pages	146-160
Number of pages	15
ISBN (Print)	3540615113, 9783540615118
DOIs	https://doi.org/10.1007/3-540-61511-3_76
State	Published - Jan 1 1996
Externally published	Yes
Event	13th International Conference on Automated Deduction, CADE 1996 - New Brunswick, United States Duration: Jul 30 1996 → Aug 3 1996

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1104
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	13th International Conference on Automated Deduction, CADE 1996
Country	United States
City	New Brunswick
Period	7/30/96 → 8/3/96

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/3-540-61511-3_76

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

Cite this

Suttner, C. B., & Sutcliffe, G. (1996). The design of the CADE-13 ATP system competition. In J. K. Slaney, & M. A. McRobbie (Eds.), Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings (pp. 146-160). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1104). Springer Verlag. https://doi.org/10.1007/3-540-61511-3_76

The design of the CADE-13 ATP system competition. / Suttner, Christian B.; Sutcliffe, Geoff.

Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. ed. / John K. Slaney; Michael A. McRobbie. Springer Verlag, 1996. p. 146-160 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1104).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Suttner, CB & Sutcliffe, G 1996, The design of the CADE-13 ATP system competition. in JK Slaney & MA McRobbie (eds), Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1104, Springer Verlag, pp. 146-160, 13th International Conference on Automated Deduction, CADE 1996, New Brunswick, United States, 7/30/96. https://doi.org/10.1007/3-540-61511-3_76

Suttner CB, Sutcliffe G. The design of the CADE-13 ATP system competition. In Slaney JK, McRobbie MA, editors, Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. Springer Verlag. 1996. p. 146-160. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-61511-3_76

Suttner, Christian B. ; Sutcliffe, Geoff. / The design of the CADE-13 ATP system competition. Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. editor / John K. Slaney ; Michael A. McRobbie. Springer Verlag, 1996. pp. 146-160 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{13ff3a08e252463fbe0043243e713a41,

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 are to contribute to the evaluation of ATP systems, to stimulate ATP research and system development, and to expose ATP systems to interested researchers both within and outside the ATP community. This paper identifies and discusses the issues that determine the nature of the competition. Choices and motivated decisions, with respect to the issues, are given.",

author = "Suttner, {Christian B.} and Geoff Sutcliffe",

year = "1996",

month = jan,

day = "1",

doi = "10.1007/3-540-61511-3_76",

language = "English (US)",

isbn = "3540615113",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "146--160",

editor = "Slaney, {John K.} and McRobbie, {Michael A.}",

booktitle = "Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings",

note = "13th International Conference on Automated Deduction, CADE 1996 ; Conference date: 30-07-1996 Through 03-08-1996",

}

TY - GEN

T1 - The design of the CADE-13 ATP system competition

AU - Suttner, Christian B.

AU - Sutcliffe, Geoff

PY - 1996/1/1

Y1 - 1996/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 are to contribute to the evaluation of ATP systems, to stimulate ATP research and system development, and to expose ATP systems to interested researchers both within and outside the ATP community. This paper identifies and discusses the issues that determine the nature of the competition. Choices and motivated decisions, 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 are to contribute to the evaluation of ATP systems, to stimulate ATP research and system development, and to expose ATP systems to interested researchers both within and outside the ATP community. This paper identifies and discusses the issues that determine the nature of the competition. Choices and motivated decisions, with respect to the issues, are given.

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

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

U2 - 10.1007/3-540-61511-3_76

DO - 10.1007/3-540-61511-3_76

M3 - Conference contribution

AN - SCOPUS:0013212232

SN - 3540615113

SN - 9783540615118

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 146

EP - 160

BT - Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings

A2 - Slaney, John K.

A2 - McRobbie, Michael A.

PB - Springer Verlag

T2 - 13th International Conference on Automated Deduction, CADE 1996

Y2 - 30 July 1996 through 3 August 1996

ER -