The TPTP problem library

Geoffrey 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
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

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.