The TPTP Problem Library and Associated Infrastructure
The TPTP Problem Library and Associated Infrastructure
复制标题
DOI：
10.1007/s10817-017-9407-7
复制
发表时间：
2017-12-01
期刊：
影响因子：
--
通讯作者：
Sutcliffe, Geoff
中科院分区：
文献类型：
--
作者：
Sutcliffe, Geoff
本文描述了TPTP题库及其相关的基础设施，从使用子句范式(CNF)，到一阶形式(FOF)和类型化一阶形式(TFF)，再到单态类型化高阶形式(TH0)。TPTP v6.4.0是引入多态类型高阶表单之前的最后一个版本，因此用作样本。本文概述了TPTP的目标和历史，记录了其发展到6.4.0版本，回顾了TPTP问题的结构和内容，并概述了与TPTP相关的基础设施。
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.