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.

• Type: Journal
• Year: 2010
• Where: LOGCOM
• Authors: Philippe Balbiani, Hans P. van Ditmarsch, Andreas Herzig, Tiago De Lima
• Keywords: Deterministic Polynomial Space, Labelled Tableau Calculus, LOGCOM 2010, Multi-agent Epistemic Logic