LILaC
- paper abstract
A tableau method for public announcement logics
Balbiani, Philippe and Ditmarsch, Hans van and Herzig, Andreas and Lima, Tiago de
Abstract:
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.
Note:
A preliminary version was published in the proceedings of TABLEAUX 2007
under the title
``A tableau method for public announcement logics''
(
PDF)
Bibtex-entry:
https://www.irit.fr/~Andreas.Herzig