Tableaux for public announcement logic

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

Research output: Contribution to journalArticleAcademicpeer-review

25 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

Tableaux
Polynomials
Logic
Epistemic Logic
Tableau
Calculus
Entire
Polynomial
Operator
Public Announcement
Model
Satisfiability
Calculi

Cite this

Balbiani, P., Ditmarsch, van, H., Herzig, A., & Lima, de, T. (2010). Tableaux for public announcement logic. Journal of Logic and Computation, 20(1), 55-76. https://doi.org/10.1093/logcom/exn060
Balbiani, Philippe ; Ditmarsch, van, H. ; Herzig, Andreas ; Lima, de, T. / Tableaux for public announcement logic. In: Journal of Logic and Computation. 2010 ; Vol. 20, No. 1. pp. 55-76.
@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",

}

Balbiani, P, Ditmarsch, van, H, Herzig, A & Lima, de, T 2010, 'Tableaux for public announcement logic', Journal of Logic and Computation, vol. 20, no. 1, pp. 55-76. https://doi.org/10.1093/logcom/exn060

Tableaux for public announcement logic. / Balbiani, Philippe; Ditmarsch, van, H.; Herzig, Andreas; Lima, de, T.

In: Journal of Logic and Computation, Vol. 20, No. 1, 2010, p. 55-76.

Research output: Contribution to journalArticleAcademicpeer-review

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

VL - 20

SP - 55

EP - 76

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

SN - 0955-792X

IS - 1

ER -

Balbiani P, Ditmarsch, van H, Herzig A, Lima, de T. Tableaux for public announcement logic. Journal of Logic and Computation. 2010;20(1):55-76. https://doi.org/10.1093/logcom/exn060