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

Geoff Sutcliffe

doi:10.1007/s10817-009-9143-8

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

Geoff Sutcliffe

Computer Science

Research output: Contribution to journal › Article

255 Scopus citations

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 language	English (US)
Pages (from-to)	337-362
Number of pages	26
Journal	Journal of Automated Reasoning
Volume	43
Issue number	4
DOIs	https://doi.org/10.1007/s10817-009-9143-8
State	Published - Jan 2009

Keywords

ATP system evaluation
TPTP

ASJC Scopus subject areas

Software
Computational Theory and Mathematics
Artificial Intelligence

Access to Document

10.1007/s10817-009-9143-8

Cite this

Sutcliffe, G. (2009). The TPTP problem library and associated infrastructure: ttthe FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning, 43(4), 337-362. https://doi.org/10.1007/s10817-009-9143-8

@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 = "Geoff Sutcliffe",

year = "2009",

month = jan,

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, Geoff

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 -