Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite

Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite
复制标题

定理证明者合作：结合 HOL-Light 和 CVC Lite 的案例研究

DOI：
10.1016/j.entcs.2005.12.005
复制
发表时间：
2005
期刊：
ArXiv
影响因子：
--
通讯作者：
Yeting Ge
Yeting Ge
中科院分区：
--
文献类型：
--
作者：
Sean McLaughlin;Clark W. Barrett;Yeting Ge

文献摘要

被引文献

相似文献

本文是一个结合定理证明器的案例研究。我们在HOL-Light中定义了一个派生规则CVC_PROVE，它调用CVC Lite并将生成的证明对象转换回HOL-Light。因此，我们为CVC Lite获得了高度可信的校对器，同时也从根本上扩展了HOL-Light的功能。
This paper is a case study in combining theorem provers. We define a derived rule in HOL-Light, CVC_PROVE, which calls CVC Lite and translates the resulting proof object back to HOL-Light. As a result, we obtain a highly trusted proof-checker for CVC Lite, while also fundamentally expanding the capabilities of HOL-Light.