The TPTP Problem Library: CNF Release v1.2.1

Geoffrey Sutcliffe, Christian Suttner

Research output: Contribution to journalArticle

188 Citations (Scopus)

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
StatePublished - 1998
Externally publishedYes

Fingerprint

Utility programs
Theorem proving
Statistics
Internet

Keywords

  • Experimental evaluation
  • Problem library
  • TPTP

ASJC Scopus subject areas

  • Artificial Intelligence

Cite this

The TPTP Problem Library : CNF Release v1.2.1. / Sutcliffe, Geoffrey; Suttner, Christian.

In: Journal of Automated Reasoning, Vol. 21, No. 2, 1998, p. 177-203.

Research output: Contribution to journalArticle

Sutcliffe, Geoffrey ; Suttner, Christian. / The TPTP Problem Library : CNF Release v1.2.1. In: Journal of Automated Reasoning. 1998 ; Vol. 21, No. 2. pp. 177-203.
@article{bf006f958f64436595923513777d1801,
title = "The TPTP Problem Library: CNF Release v1.2.1",
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.",
keywords = "Experimental evaluation, Problem library, TPTP",
author = "Geoffrey Sutcliffe and Christian Suttner",
year = "1998",
language = "English (US)",
volume = "21",
pages = "177--203",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "2",

}

TY - JOUR

T1 - The TPTP Problem Library

T2 - CNF Release v1.2.1

AU - Sutcliffe, Geoffrey

AU - Suttner, Christian

PY - 1998

Y1 - 1998

N2 - 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.

AB - 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.

KW - Experimental evaluation

KW - Problem library

KW - TPTP

UR - http://www.scopus.com/inward/record.url?scp=0032186666&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0032186666&partnerID=8YFLogxK

M3 - Article

VL - 21

SP - 177

EP - 203

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 2

ER -