Sciweavers

LOGCOM
2010

Tableaux for Public Announcement Logic

13 years 2 months ago
Tableaux for Public Announcement Logic
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.
Philippe Balbiani, Hans P. van Ditmarsch, Andreas
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LOGCOM
Authors Philippe Balbiani, Hans P. van Ditmarsch, Andreas Herzig, Tiago De Lima
Comments (0)