Tableaux for Non-normal Public Announcement Logic
Tableaux for Non-normal Public Announcement Logic
复制标题
DOI：
10.1007/978-3-662-45824-2_9
复制
发表时间：
2015-01
期刊：
影响因子：
--
通讯作者：
Minghui Ma;Katsuhiko Sano;François Schwarzentruber;F. R. Velázquez-Quesada
中科院分区：
文献类型：
--
作者：
Minghui Ma;Katsuhiko Sano;François Schwarzentruber;F. R. Velázquez-Quesada
本文提出了一种表格演算，用于单调邻域模型上的公告的两种语义解释：交集语义和子集语义，由 Ma 和 Sano 开发。我们证明这两种演算在其相应的语义解释方面都是健全和完整的，而且，我们确定该公告扩展的可满足性问题在这两种情况下都是 NP 完全的。表格演算已在 Lotrecscheme 中实现。
This paper presents a tableau calculus for two semantic interpretations of public announcements over monotone neighbourhood models: the intersection and the subset semantics, developed by Ma and Sano. We show that both calculi are sound and complete with respect to their corresponding semantic interpretations and, moreover, we establish that the satisfiability problem of this public announcement extensions is NP-complete in both cases. The tableau calculi has been implemented in Lotrecscheme.