Tableaux for Public Announcement Logic
Tableaux for Public Announcement Logic
复制标题
公告逻辑的 Tableaux
DOI：
10.1093/logcom/exn060
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
T. Lima
中科院分区：
文献类型：
--
作者：
P. Balbiani;H. V. Ditmarsch;A. Herzig;T. Lima
公共公告逻辑通过动态运算符扩展了多智能体认知逻辑，对整个智能体组的公告信息后果进行建模。本文给出了该逻辑的标记表演算，并证明了它决定了确定多项式空间中公式的可满足性。由于已知这个问题是pspace完备的，因此我们的证明方法是最优的。
Public announcement logic extends multi-agent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. In this article, we propose a labelled tableau calculus for this logic, and show that it decides satisfiability of formulas in deterministic polynomial space. Since this problem is known to be PSPACE-complete, it follows that our proof method is optimal.