主要证据
- HOL(y)Hammer: Online ATP Service for HOL LightS1 · 主要研究来源 · 论文 · 2013-09-19
HOL(y)Hammer 将学习式前提选择与 ATP 接入 HOL Light
用户可以上传 HOL Light 工程，并让服务使用学习式相关性模型、并行 ATP 组合与决策过程处理新猜想。
发生了什么？
Kaliszyk 与 Urban 于 2013 年 9 月 19 日发布 HOL(y)Hammer，将基于项目证明训练的多种前提选择方法与多个自动定理证明器结合为在线 AI/ATP 服务。
为什么重要？
它较早展示了机器学习如何作为成熟服务嵌入证明助手，并在大规模形式数学库上工作。
重要性说明：HOL(y)Hammer 将机器学习前提选择与多个自动推理系统部署为面向大型 HOL Light 工程的在线服务，使 large-theory AI/ATP 方法进入日常形式数学流程。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 实质性支持
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 学习模型选择前提，自动证明器搜索证明，用户在 HOL Light 工程中提供目标猜想。
- 人类贡献
- 研究者工程化实现服务、学习方法、ATP 组合、项目处理与交互接口。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-15
技术细节
- 系统
- holyhammer, hol-light
- 机构
- university-of-innsbruck
- 数学问题
- higher-order-logic-theorem-proving
- 方法
- machine-learning, premise-selection, automated-theorem-proving, portfolio-reasoning
全部来源与工件
- HOL(y)Hammer: Online ATP Service for HOL LightS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
验证历史
- 2013-09-19 · 论文已发布 · E2 · 研究记录
arXiv 研究记录确认服务架构及论文报告的 HOL Light 部署。
更正
当前没有记录的更正。