The TPTP Problem Library: CNF Release v1.2.1

Geoff Sutcliffe, Christian Suttner

Research output: Contribution to journalArticlepeer-review

194 Scopus citations

Abstract

This paper provides a detailed description of the CNF part of the TPTP Problem Library for automated theorem-proving systems. The library is available via the Internet and forms a common basis for development and experimentation with automated theorem provers. This paper explains the motivations and reasoning behind the development of the TPTP (thus implicitly explaining the design decisions made) and describes the TPTP contents and organization. It also provides guidelines for obtaining and using the library, summary statistics about release v1.2.1, and an overview of the tptp2X utility program. References for all the sources of TPTP problems are provided.

Original languageEnglish (US)
Pages (from-to)177-203
Number of pages27
JournalJournal of Automated Reasoning
Volume21
Issue number2
DOIs
StatePublished - Jan 1 1998
Externally publishedYes

Keywords

  • Experimental evaluation
  • Problem library
  • TPTP

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'The TPTP Problem Library: CNF Release v1.2.1'. Together they form a unique fingerprint.

Cite this