PAL·S5在证明辅助器中的形式化
计算机科学中的逻辑
2020-12-18 v1
摘要
作为将证明辅助器应用于逻辑研究的一项实验，我们在Lean定理证明器中形式化了带有PAL风格动态模态的多智能体模态逻辑S5的模型与证明系统。我们给出了公开宣告归约公理以及模态逻辑S5的可靠性与完备性的形式化证明，该证明可使用Lean 3.19.0进行类型检查。完整的证明现已发布于Github。
引用
@article{arxiv.2012.09388,
title = {Formalization of PAL$\cdot$S5 in Proof Assistant},
author = {Jiatu Li},
journal= {arXiv preprint arXiv:2012.09388},
year = {2020}
}
备注
For proof codes, see https://github.com/ljt12138/Formalization-PAL