The TPTP problem library

Geoff Sutcliffe, Christian Suttner, Theodor Yemenis

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

98 Scopus citations


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
Number of pages15
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


Other12th International Conference on Automated Deduction, CADE-12 1994

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this