Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure
复制标题
使用 TPTP THF 基础设施进行高阶逻辑自动推理
DOI：
--
复制
发表时间：
2010
影响因子：
--
通讯作者：
Christoph Benzmüller
中科院分区：
文献类型：
--
作者：
G. Sutcliffe;Christoph Benzmüller
Thousands of Problems for Theorem Provers（TPTP）问题库是一个众所周知的基础设施，支持自动定理证明（ATP）系统的研究，开发和部署。TPTP从一阶形式（FOF）逻辑到类型化高阶形式（THF）逻辑的扩展，为高阶逻辑ATP系统的新开发和应用提供了基础。关键的发展是THF语言的规范，TPTP中高阶问题的增加，TPTP THF基础设施的发展，高阶逻辑的几个ATP系统，以及高阶ATP在一系列领域的使用。本文介绍了这些发展。
The Thousands of Problems for Theorem Provers (TPTP) problem library is the basis of a well known and well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The extension of the TPTP from first-order form (FOF) logic to typed higher-order form (THF) logic has provided a basis for new development and application of ATP systems for higher-order logic. Key developments have been the specification of the THF language, the addition of higher-order problems to the TPTP, the development of the TPTP THF infrastructure, several ATP systems for higher-order logic, and the use of higher-order ATP in a range of domains. This paper describes these developments.