在证明助手间共享库：面向 HOL 系列
计算机科学中的逻辑
2018-07-06 v1
摘要
我们今天观察到证明系统的高度多样性。这种多样性带来一个负面后果，即大量定理被反复证明。与编程语言不同，这些系统难以协作，因为它们未实现相同的逻辑。逻辑框架是一类能通过实现多种逻辑来克服此问题的定理证明器。在本工作中，我们研究 STTforall 逻辑，这是已编码于逻辑框架 Dedukti 中的简单类型论扩展。我们给出从该逻辑到 OpenTheory 的翻译，OpenTheory 是一个面向 HOL 系列证明器的证明系统与互操作工具。我们利用此翻译将一个包含费马小定理的算术库导出至 OpenTheory 以及 Coq 与 Matita 另外两个证明系统。
引用
@article{arxiv.1807.01873,
title = {Sharing a Library between Proof Assistants: Reaching out to the HOL Family},
author = {François Thiré},
journal= {arXiv preprint arXiv:1807.01873},
year = {2018}
}
备注
In Proceedings LFMTP 2018, arXiv:1807.01352