Automated Certified Proofs with CiME3

Automated Certified Proofs with CiME3
复制标题

使用 CiME3 进行自动认证校样

DOI：
--
复制
发表时间：
2011
期刊：
International Conference on Rewriting Techniques and Applications
影响因子：
--
通讯作者：
X. Urbain
X. Urbain
中科院分区：
--
文献类型：
--
作者：
Évelyne Contejean;Pierre Courtieu;Julien Forest;O. Pons;X. Urbain

文献摘要

被引文献

相似文献

我们提出了重写工具包CiME3。其他原创 功能，这个版本享有两种引擎：处理和 发现重写系统的各种属性的证明，并 从认证问题中给出的证明轨迹生成Coq脚本 格式，以证明他们与怀疑证明助理一样， 鸡因此，这些功能为使用CiME3添加 自动化证明终止或合流在正式的 在Coq证明助理的发展。
We present the rewriting toolkit CiME3. Amongst other original features, this version enjoys two kinds of engines: to handle and discover proofs of various properties of rewriting systems, and to generate Coq scripts from proof traces given in certification problem format in order to certify them with a skeptical proof assistant like Coq. Thus, these features open the way for using CiME3 to add automation to proofs of termination or confluence in a formal development in the Coq proof assistant.