Stalnaker 信念逻辑在 Isabelle/HOL 中的实现
计算机科学中的逻辑
2024-04-24 v1
摘要
形式化模型的基础常依赖于诸如 S4 和 S4.2 及其语义所涉及的模态逻辑的某些逻辑方面；然而，这些数学结果常以未包含详细证明或参考的形式出现在论文或书籍中，无法让读者自行验证。 我们通过在 Isabelle/HOL 中形式化其 soundness 与 completeness 结果，强化了信念逻辑 S4.2 的基础。该逻辑对应于 Stalnaker 系统中仅包含信念模态的知识片段。 此外，我们形式化了两种 S4 公理化之间的等价性，这两种公理化分别用于不同的语义：一种常用于关系语义，另一种则源于拓扑语义。
关键词
引用
@article{arxiv.2404.14919,
title = {Stalnaker's Epistemic Logic in Isabelle/HOL},
author = {Laura P. Gamboa Guzman and Kristin Y. Rozier},
journal= {arXiv preprint arXiv:2404.14919},
year = {2024}
}
备注
In Proceedings LSFA/HCVS 2023, arXiv:2404.13672