主要证据
- TPTP HistoryS1 · 主要研究来源 · 基准
TPTP 建立自动定理证明共享基准问题库
TPTP 以统一格式整理 ATP 测试问题，并建立领域分类与版本发布规范，使定理证明器能够在可比较输入上进行测试。
发生了什么？
TPTP 官方历史记录显示，首个公开版本 v1.0.0 于 1993 年 11 月 12 日星期五发布，包含 23 个领域、2,295 个问题。
为什么重要？
该问题库成为自动演绎核心基础设施，并进一步支撑系统竞赛、benchmark 与学习式定理证明。
重要性说明：TPTP 将大型自动定理证明问题库标准化并公开，使可重复评测和跨系统比较建立在共同语料基础上。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 尚属声明
- 证据等级
- E3 · 可检查工件
- AI 角色
- 仅计算支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- AI 与 ATP 系统在该问题库上接受评测；事件本身是 benchmark 基础设施而非 AI 生成数学结果。
- 人类贡献
- Geoff Sutcliffe、Christian Suttner 与贡献者整理、标准化并维护公共问题库。
- 验证状态
- 尚属声明 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-15
技术细节
- 系统
- tptp
- 机构
- —
- 数学问题
- automated-theorem-proving
- 方法
- benchmarking, standardized-problem-formats
全部来源与工件
- TPTP HistoryS1 · 主要研究来源 · 基准 · 访问于 2026-09-15
- TPTP Problem Library工件 · 基准
验证历史
- 1993-11-12 · 尚属声明 · E3 · 可检查工件
TPTP 官方历史与当前问题库使发布 chronology 与 benchmark artifacts 可直接检查。
更正
当前没有记录的更正。