Goal Translation for a Hammer for Coq
Goal Translation for a Hammer for Coq
复制标题
DOI：
10.4204/eptcs.210.4
复制
发表时间：
2016-01-01
影响因子：
--
通讯作者：
Kaliszyk, Cezary
中科院分区：
文献类型：
--
作者：
Czajka, Lukasz;Kaliszyk, Cezary
锤子是为正式证明助手提供通用自动化的工具。尽管类型理论的更高级版本的流行度，但对于此类系统来说，毫无疑问。我们将各种锤子组件的扩展为键入理论：（i）将COQ逻辑的大部分转换为自动证明系统的格式； （ii）基于Ben-Yelles型算法的证明重建机制，结合了有限的重写，一致性关闭和对Dyckhoff系统LJT左规则的一阶概括。
Hammers are tools that provide general purpose automation for formal proof assistants. Despite the gaining popularity of the more advanced versions of type theory, there are no hammers for such systems. We present an extension of the various hammer components to type theory: (i) a translation of a significant part of the Coq logic into the format of automated proof systems; (ii) a proof reconstruction mechanism based on a Ben-Yelles-type algorithm combined with limited rewriting, congruence closure and a first-order generalization of the left rules of Dyckhoff's system LJT.