Kripke 结构的代数推广
逻辑
2009-11-13 v1 计算机科学中的逻辑
环与代数
摘要
经典命题正规模态逻辑的 Kripke 语义通过将 Kripke 结构嵌入到更广泛的点状稳定支撑量帧（pointed stably supported quantales）类中而得以代数化。这种代数语义涵盖了基于带一元算子的格的传统代数语义，并暗示了模态逻辑的自然解释，这些解释通过拓扑群胚和逆半群，在几何与分析中出现的结构（如叶状流形和算子代数）中可能具有应用价值。我们研究了基于量帧的语义对于系统 K、T、K4、S4 和 S5 的完备性性质，特别是获得了不使用否定或模态必然算子的 S5 公理化体系。作为补充示例，我们描述了直觉主义命题模态逻辑、程序逻辑 PDL 以及分层时序逻辑 CTL。
引用
@article{arxiv.0704.1886,
title = {An algebraic generalization of Kripke structures},
author = {Sérgio Marcelino and Pedro Resende},
journal= {arXiv preprint arXiv:0704.1886},
year = {2009}
}
评论
39 pages