Hammer for Coq: Automation for Dependent Type Theory.
Hammer for Coq: Automation for Dependent Type Theory.
复制标题
DOI：
10.1007/s10817-018-9458-4
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Kaliszyk C
中科院分区：
文献类型：
--
作者：
Czajka Ł;Kaliszyk C
锤子为基于HOL和集合论的证明助手提供了最强大的通用自动化。尽管基于归纳构造演算的更高级版本的类型理论越来越受欢迎，但迄今为止，由于缺乏翻译和重建组件，这些基础的构建一直受到阻碍。在本文中，我们提出了一个依赖类型理论的全锤结构及其Coq证明助手的实现。锤子的一个关键组成部分是从归纳构造的演算（带有Coq引入的某些扩展）到无类型一阶逻辑的建议翻译。翻译是“足够”健全和完整的，可用于自动定理证明。我们还介绍了一种基于eauto-type算法的证明重构机制，该算法结合了有限重写、同余闭包和前向推理。该算法能够在Coq逻辑中重新证明atp建立的大多数定理。与基于机器学习的相关前提选择一起，这构成了一个完整的锤子系统。在一个模拟Coq标准库开发的引导场景中，对整个过程的性能进行了评估。对于库中的每个定理，只能使用以前的定理和证明。我们证明，在8个cpu的系统上，40.8%的定理可以在大约40秒的实时时间内在按钮模式下被证明。
Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive Constructions, the construction of hammers for such foundations has been hindered so far by the lack of translation and reconstruction components. In this paper, we present an architecture of a full hammer for dependent type theory together with its implementation for the Coq proof assistant. A key component of the hammer is a proposed translation from the Calculus of Inductive Constructions, with certain extensions introduced by Coq, to untyped first-order logic. The translation is “sufficiently” sound and complete to be of practical use for automated theorem provers. We also introduce a proof reconstruction mechanism based on an eauto-type algorithm combined with limited rewriting, congruence closure and some forward reasoning. The algorithm is able to re-prove in the Coq logic most of the theorems established by the ATPs. Together with machine-learning based selection of relevant premises this constitutes a full hammer system. The performance of the whole procedure is evaluated in a bootstrapping scenario emulating the development of the Coq standard library. For each theorem in the library only the previous theorems and proofs can be used. We show that 40.8% of the theorems can be proved in a push-button mode in about 40 s of real time on a 8-CPU system.
登录
查看更多内容
DOI：
10.1007/s10817-016-9362-8
发表时间：
2016-10-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Blanchette, Jasmin Christian;Greenaway, David;Urban, Josef
通讯作者：
Urban, Josef
DOI：
10.1007/s10817-013-9286-5
发表时间：
2014-02-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Alama, Jesse;Heskes, Tom;Urban, Josef
通讯作者：
Urban, Josef
影响因子：
1
作者：
COQUAND, T;HUET, G
通讯作者：
HUET, G
DOI：
10.4204/eptcs.210.4
发表时间：
2016-01-01
影响因子：
--
作者：
Czajka, Lukasz;Kaliszyk, Cezary
通讯作者：
Kaliszyk, Cezary
影响因子：
--
作者：
Blanchette, Jasmin C.;Kaliszyk, Cezary;Urban, Josef
通讯作者：
Urban, Josef