The TPTP problem library

Geoff Sutcliffe, Christian Suttner, Theodor Yemenis

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

90 Scopus citations

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
EditorsAlan Bundy
PublisherSpringer Verlag
Pages252-266
Number of pages15
ISBN (Print)9783540581567
DOIs
StatePublished - 1994
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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The TPTP problem library'. Together they form a unique fingerprint.

  • Cite this

    Sutcliffe, G., Suttner, C., & Yemenis, T. (1994). The TPTP problem library. In A. Bundy (Ed.), Automated Deduction — CADE-12 - 12th International Conference on Automated Deduction, Proceedings (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. https://doi.org/10.1007/3-540-58156-1_18