Tableaux for public announcement logic

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

doi:10.1093/logcom/exn060

Tableaux for public announcement logic

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

Philosophy & Ethics

Research output: Contribution to journal › Article › Academic › peer-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 language	English
Pages (from-to)	55-76
Number of pages	22
Journal	Journal of Logic and Computation
Volume	20
Issue number	1
DOIs	https://doi.org/10.1093/logcom/exn060
Publication status	Published - 2010

Access to Document

10.1093/logcom/exn060

Cite this

@article{f5eabcada3264c48a1772b8383e562a0,

title = "Tableaux for public announcement logic",

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.",

author = "Philippe Balbiani and {Ditmarsch, van}, H. and Andreas Herzig and {Lima, de}, T.",

year = "2010",

doi = "10.1093/logcom/exn060",

language = "English",

volume = "20",

pages = "55--76",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

publisher = "Oxford University Press",

number = "1",

}

TY - JOUR

T1 - Tableaux for public announcement logic

AU - Balbiani, Philippe

AU - Ditmarsch, van, H.

AU - Herzig, Andreas

AU - Lima, de, T.

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1093/logcom/exn060

DO - 10.1093/logcom/exn060

M3 - Article

SN - 0955-792X

VL - 20

SP - 55

EP - 76

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 1

ER -

Tableaux for public announcement logic

Abstract

Access to Document

Fingerprint

Cite this