Tableaux for public announcement logic

Philippe Balbiani, H. Ditmarsch, van, Andreas Herzig, T. Lima, de

Research output: Contribution to journalArticleAcademicpeer-review

35 Citations (Scopus)

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.
Original languageEnglish
Pages (from-to)55-76
Number of pages22
JournalJournal of Logic and Computation
Volume20
Issue number1
DOIs
Publication statusPublished - 2010

Fingerprint

Dive into the research topics of 'Tableaux for public announcement logic'. Together they form a unique fingerprint.

Cite this