终止性证书的自动化验证
计算机科学中的逻辑
2012-12-12 v1 数学软件
软件工程
摘要
为了增强用户信心，许多自动定理证明器提供了可独立验证的证书。在本文中，我们报告了在开发用于检查项重写系统终止性证书正确性的独立工具方面取得的进展，并在证明助手 Coq 中形式化地证明了其正确性。为此，我们利用了 Coq 的提取机制以及名为 CoLoR 的重写理论与终止性库。
引用
@article{arxiv.1212.2350,
title = {Automated verification of termination certificates},
author = {Frédéric Blanqui and Kim Quyen Ly},
journal= {arXiv preprint arXiv:1212.2350},
year = {2012}
}