The TPTP problem library

Geoffrey Sutcliffe, Christian Suttner, Theodor Yemenis

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

89 Citations (Scopus)

Abstract

This paper provides a description of the TPTP library of problems for automated theorem provers. The library is available via Internet, and is intended to form a common basis for the development of and experimentation with automated theorem provers. To support this goal, this paper provides: —the motivations for building the library; —a description of the library structure including overview information; —a description of the tptp2X utility program; —guidelines for obtaining and using the library.

Original languageEnglish (US)
Title of host publicationAutomated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings
PublisherSpringer Verlag
Pages252-266
Number of pages15
Volume814 LNAI
ISBN (Print)9783540581567
StatePublished - 1994
Externally publishedYes
Event12th International Conference on Automated Deduction, CADE-12 1994 - Nancy, France
Duration: Jun 26 1994Jul 1 1994

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume814 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other12th International Conference on Automated Deduction, CADE-12 1994
CountryFrance
CityNancy
Period6/26/947/1/94

Fingerprint

Utility programs
Theorem
Experimentation
Libraries
Internet

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Sutcliffe, G., Suttner, C., & Yemenis, T. (1994). The TPTP problem library. In Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings (Vol. 814 LNAI, pp. 252-266). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 814 LNAI). Springer Verlag.

The TPTP problem library. / Sutcliffe, Geoffrey; Suttner, Christian; Yemenis, Theodor.

Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings. Vol. 814 LNAI Springer Verlag, 1994. p. 252-266 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 814 LNAI).

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

Sutcliffe, G, Suttner, C & Yemenis, T 1994, The TPTP problem library. in Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings. vol. 814 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 814 LNAI, Springer Verlag, pp. 252-266, 12th International Conference on Automated Deduction, CADE-12 1994, Nancy, France, 6/26/94.
Sutcliffe G, Suttner C, Yemenis T. The TPTP problem library. In Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings. Vol. 814 LNAI. Springer Verlag. 1994. p. 252-266. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Sutcliffe, Geoffrey ; Suttner, Christian ; Yemenis, Theodor. / The TPTP problem library. Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings. Vol. 814 LNAI Springer Verlag, 1994. pp. 252-266 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{567b68647b7e4a7da139bcfcb63867c3,
title = "The TPTP problem library",
abstract = "This paper provides a description of the TPTP library of problems for automated theorem provers. The library is available via Internet, and is intended to form a common basis for the development of and experimentation with automated theorem provers. To support this goal, this paper provides: —the motivations for building the library; —a description of the library structure including overview information; —a description of the tptp2X utility program; —guidelines for obtaining and using the library.",
author = "Geoffrey Sutcliffe and Christian Suttner and Theodor Yemenis",
year = "1994",
language = "English (US)",
isbn = "9783540581567",
volume = "814 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "252--266",
booktitle = "Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings",

}

TY - GEN

T1 - The TPTP problem library

AU - Sutcliffe, Geoffrey

AU - Suttner, Christian

AU - Yemenis, Theodor

PY - 1994

Y1 - 1994

N2 - This paper provides a description of the TPTP library of problems for automated theorem provers. The library is available via Internet, and is intended to form a common basis for the development of and experimentation with automated theorem provers. To support this goal, this paper provides: —the motivations for building the library; —a description of the library structure including overview information; —a description of the tptp2X utility program; —guidelines for obtaining and using the library.

AB - This paper provides a description of the TPTP library of problems for automated theorem provers. The library is available via Internet, and is intended to form a common basis for the development of and experimentation with automated theorem provers. To support this goal, this paper provides: —the motivations for building the library; —a description of the library structure including overview information; —a description of the tptp2X utility program; —guidelines for obtaining and using the library.

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

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

M3 - Conference contribution

SN - 9783540581567

VL - 814 LNAI

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

SP - 252

EP - 266

BT - Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings

PB - Springer Verlag

ER -