Interacting with Modal Logics in the Coq Proof Assistant
Interacting with Modal Logics in the Coq Proof Assistant
复制标题
在 Coq Proof Assistant 中与模态逻辑交互
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
B. W. Paleo
中科院分区：
文献类型：
--
作者：
Christoph Benzmüller;B. W. Paleo
本文描述了一种在余弦证明助手中嵌入高阶模态逻辑的方法。CoQ的功能用于以最低限度的方式实现模态逻辑，但这对于重要的、非平凡的模态逻辑证明的形式化来说是足够的。从用户的角度来看，这种方法的优雅、灵活和方便，这里通过戈德尔的本体论论证的成功形式化来说明。
This paper describes an embedding of higher-order modal logics in the Coq proof assistant. Coq’s capabilities are used to implement modal logics in a minimalistic manner, which is nevertheless sufficient for the formalization of significant, non-trivial modal logic proofs. The elegance, flexibility and convenience of this approach, from a user perspective, are illustrated here with the successful formalization of Godel’s ontological argument.