The TPTP problem library and associated infrastructure: ttthe FOF and CNF Parts, v3.5.0

Research output: Contribution to journalArticle

248 Citations (Scopus)

Abstract

This paper describes the First-Order Form (FOF) and Clause Normal Form (CNF) parts of the TPTP problem library, and the associated infrastructure. TPTP v3.5.0 was the last release containing only FOF and CNF problems, and thus serves as the exemplar. This paper summarizes the history and development of the TPTP, describes the structure and contents of the TPTP, and gives an overview of TPTP related projects and tools.

Original languageEnglish (US)
Pages (from-to)337-362
Number of pages26
JournalJournal of Automated Reasoning
Volume43
Issue number4
DOIs
StatePublished - Jan 2009

Keywords

  • ATP system evaluation
  • TPTP

ASJC Scopus subject areas

  • Artificial Intelligence
  • Software
  • Computational Theory and Mathematics

Cite this

The TPTP problem library and associated infrastructure : ttthe FOF and CNF Parts, v3.5.0. / Sutcliffe, Geoffrey.

In: Journal of Automated Reasoning, Vol. 43, No. 4, 01.2009, p. 337-362.

Research output: Contribution to journalArticle

@article{f2bf40c84a3647db82db991397768417,
title = "The TPTP problem library and associated infrastructure: ttthe FOF and CNF Parts, v3.5.0",
abstract = "This paper describes the First-Order Form (FOF) and Clause Normal Form (CNF) parts of the TPTP problem library, and the associated infrastructure. TPTP v3.5.0 was the last release containing only FOF and CNF problems, and thus serves as the exemplar. This paper summarizes the history and development of the TPTP, describes the structure and contents of the TPTP, and gives an overview of TPTP related projects and tools.",
keywords = "ATP system evaluation, TPTP",
author = "Geoffrey Sutcliffe",
year = "2009",
month = "1",
doi = "10.1007/s10817-009-9143-8",
language = "English (US)",
volume = "43",
pages = "337--362",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "4",

}

TY - JOUR

T1 - The TPTP problem library and associated infrastructure

T2 - ttthe FOF and CNF Parts, v3.5.0

AU - Sutcliffe, Geoffrey

PY - 2009/1

Y1 - 2009/1

N2 - This paper describes the First-Order Form (FOF) and Clause Normal Form (CNF) parts of the TPTP problem library, and the associated infrastructure. TPTP v3.5.0 was the last release containing only FOF and CNF problems, and thus serves as the exemplar. This paper summarizes the history and development of the TPTP, describes the structure and contents of the TPTP, and gives an overview of TPTP related projects and tools.

AB - This paper describes the First-Order Form (FOF) and Clause Normal Form (CNF) parts of the TPTP problem library, and the associated infrastructure. TPTP v3.5.0 was the last release containing only FOF and CNF problems, and thus serves as the exemplar. This paper summarizes the history and development of the TPTP, describes the structure and contents of the TPTP, and gives an overview of TPTP related projects and tools.

KW - ATP system evaluation

KW - TPTP

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

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

U2 - 10.1007/s10817-009-9143-8

DO - 10.1007/s10817-009-9143-8

M3 - Article

AN - SCOPUS:70849115250

VL - 43

SP - 337

EP - 362

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 4

ER -