将直觉主义一阶证明器集成至 Coq 的探索
计算机科学中的逻辑
2016-06-21 v1
摘要
将一个高效的直觉主义一阶证明器集成至 Coq 中，对于重放由外部自动定理证明器发现的证明非常有用。我们提出了一种两阶段方法：直觉主义证明器基于直觉主义一阶逻辑的矩阵刻画生成证书；随后该证书被翻译为相继式风格的证明。
引用
@article{arxiv.1606.05948,
title = {Towards the Integration of an Intuitionistic First-Order Prover into Coq},
author = {Fabian Kunze},
journal= {arXiv preprint arXiv:1606.05948},
year = {2016}
}
备注
In Proceedings HaTT 2016, arXiv:1606.05427