The TPTP Problem Library and Associated Infrastructure: From CNF to TH0, TPTP v6.4.0

Research output: Contribution to journalArticlepeer-review

57 Scopus citations


This paper describes the TPTP problem library and associated infrastructure, from its use of Clause Normal Form (CNF), via the First-Order Form (FOF) and Typed First-order Form (TFF), through to the monomorphic Typed Higher-order Form (TH0). TPTP v6.4.0 was the last release prior to the introduction of the polymorphic Typed Higher-order Form, and thus serves as the exemplar. This paper summarizes the aims and history of the TPTP, documents its growth up to v6.4.0, reviews the structure and contents of TPTP problems, and gives an overview of TPTP-related infrastructure.

Original languageEnglish (US)
Pages (from-to)1-20
Number of pages20
JournalJournal of Automated Reasoning
StateAccepted/In press - Feb 17 2017


  • ATP standards and tools
  • ATP system evaluation
  • TPTP

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Cite this