Isabelle/HOL 中模态逻辑立方体的系统性验证
计算机科学中的逻辑
2015-08-03 v1 人工智能
摘要
我们给出了在 Isabelle/HOL 中对著名的模态逻辑立方体进行自动化验证的工作，其中我们使用自动化推理工具证明该立方体各逻辑之间的包含关系。先前工作处理了此问题但未限于模态逻辑立方体，且使用一阶逻辑中的编码结合一阶自动化定理证明器。相比之下，我们的解法更优雅、透明且有效。它采用将量化模态逻辑嵌入经典高阶逻辑的方法。自动化推理工具，如带 LEO-II 的 Sledgehammer、Satallax 和 CVC4、Metis 以及 Nitpick，被用于实现完全自动化。尽管成功，实验也促使了对 Isabelle/HOL 工具的一些技术改进。
引用
@article{arxiv.1507.08717,
title = {Systematic Verification of the Modal Logic Cube in Isabelle/HOL},
author = {Christoph Benzmüller and Maximilian Claus and Nik Sultana},
journal= {arXiv preprint arXiv:1507.08717},
year = {2015}
}
备注
In Proceedings PxTP 2015, arXiv:1507.08375