The design of the CADE-13 ATP system competition

Christian B. Suttner, Geoffrey Sutcliffe

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

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 languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages146-160
Number of pages15
Volume1104
ISBN (Print)3540615113, 9783540615118
DOIs
StatePublished - 1996
Externally publishedYes
Event13th International Conference on Automated Deduction, CADE 1996 - New Brunswick, United States
Duration: Jul 30 1996Aug 3 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1104
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other13th International Conference on Automated Deduction, CADE 1996
CountryUnited States
CityNew Brunswick
Period7/30/968/3/96

Fingerprint

Automated Theorem Proving
Competition System
Theorem proving
System Development
Research and Development
Design
Evaluation

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Suttner, C. B., & Sutcliffe, G. (1996). The design of the CADE-13 ATP system competition. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1104, 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, Geoffrey.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1104 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 proceedingConference contribution

Suttner, CB & Sutcliffe, G 1996, The design of the CADE-13 ATP system competition. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 1104, 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 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1104. 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, Geoffrey. / The design of the CADE-13 ATP system competition. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1104 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 Geoffrey Sutcliffe",
year = "1996",
doi = "10.1007/3-540-61511-3_76",
language = "English (US)",
isbn = "3540615113",
volume = "1104",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "146--160",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

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

AU - Suttner, Christian B.

AU - Sutcliffe, Geoffrey

PY - 1996

Y1 - 1996

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

SN - 3540615113

SN - 9783540615118

VL - 1104

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

SP - 146

EP - 160

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

PB - Springer Verlag

ER -