TPTP library benchmarks

该数据集包含了708个以TFF格式的一阶问题以及717个以THF格式的高阶问题，同时排除了特定类型的问题，如包含解释算术符号的问题以及仅用于测试解析器的问题。总共有1425个问题，旨在对一阶逻辑和高阶逻辑问题上的定理证明器进行基准测试。

This dataset comprises 708 first-order problems in TFF format and 717 higher-order problems in THF format, while excluding specific types of problems such as those involving interpreted arithmetic symbols and those solely used for parser testing. In total, there are 1425 problems, and this dataset is intended to benchmark theorem provers on first-order and higher-order logical problems.

搜集汇总

背景与挑战

背景概述

该数据集是期刊文章《Superposition for Lambda-Free Higher-Order Logic》的补充实验材料，主要用于支持文章中定理证明方法的研究。它包含经过筛选的TPTP问题列表、Zipperposition定理证明器的运行脚本和配置参数，以及实验的原始输出和结果文件，旨在促进实验的复现和验证。