TPTP library benchmarks
收藏arXiv2025-09-30 收录
下载链接：
https://doi.org/10.5281/zenodo.3992618
下载链接
链接失效反馈官方服务：
资源简介：
该数据集包含了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.
提供机构：
TPTP library
