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 talk, I will present a labelled tableau calculus for this logic. It decides satisfiability of formulas in deterministic polynomial space. Since this problem is known to be PSPACE-complete, it follows that such proof method is optimal.
In the same section :