HOL(y)Hammer：面向 HOL Light 的在线自动定理证明服务
人工智能
2013-09-20 v1 数字图书馆
机器学习
计算机科学中的逻辑
数学软件
摘要
HOL(y)Hammer 是一项面向 HOL Light 系统中形式化（计算机可理解）数学的在线人工智能/自动定理证明（AI/ATP）服务。该服务允许用户上传并自动处理基于 HOL Light 的任意形式化开发（项目），并利用某些已上传项目中定义的概念来攻击任意猜想。为此，该服务结合了多个自动推理系统与多种前提选择方法，这些方法均在所有项目证明上进行了训练。服务器上现成可用于此类查询回答的项目包括 Flyspeck、多元分析与复分析库的最新版本。该服务运行于一台 48 核 CPU 服务器上，目前针对每项任务并行采用 7 种 AI/ATP 组合与 4 种决策过程以提升整体性能。该系统也可供感兴趣的用户进行本地安装，以便为其自身的证明开发进行定制。此外，还提供了一个 Emacs 接口，支持对该服务进行并行异步查询。本文概述了该服务的整体结构，讨论了所出现的问题及其解决方案，并给出了使用该系统的初步报告。
引用
@article{arxiv.1309.4962,
title = {HOL(y)Hammer: Online ATP Service for HOL Light},
author = {Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:1309.4962},
year = {2013}
}