Samenvatting
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.
Originele taal-2 | Engels |
---|---|
Pagina's (van-tot) | 55-76 |
Aantal pagina's | 22 |
Tijdschrift | Journal of Logic and Computation |
Volume | 20 |
Nummer van het tijdschrift | 1 |
DOI's | |
Status | Gepubliceerd - 2010 |