Tableaux for Public Announcement Logic

被引：27

作者：

Balbiani, Philippe ^{[1
]}

Van Ditmarsch, Hans ^{[1
,2
]}

Herzig, Andreas ^{[1
]}

De Lima, Tiago ^{[3
]}

机构：

[1] Univ Toulouse, CNRS, Inst Rech Informat Toulouse, F-31062 Toulouse 9, France

[2] Univ Otago, Dunedin 9054, New Zealand

[3] Eindhoven Univ Technol, Dept Ind Engn & Innovat Sci, NL-5600 MB Eindhoven, Netherlands

来源：

JOURNAL OF LOGIC AND COMPUTATION | 2010年 / 20卷 / 01期

关键词：

Analytic tableaux; dynamic epistemic logics; public announcement logic; knowledge representation and reasoning; multi-agent systems;

D O I：

10.1093/logcom/exn060

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：55 / 76

页数：22

共 12 条

[1]

[Anonymous], ARTIFICIAL INTELLIGE

[2]

[Anonymous], 1983, Proof Methods for Modal and Intuitionistic Logics

[3]

Balbiani P, 2007, LECT NOTES COMPUT SC, V4548, P43

[4]

Balbiani Philippe., 2007, P 11 C THEORETICAL A, P42

[5]

Baltag A., 1998, P 7 C THEOR ASP RAT, P43

[6]

de Boer M., 2007, P FORM APPR MULT SYS

[7]

GERBRANDY J, 1999, THESIS U AMSTERDAM A

[8]

Kooi B., 2007, J. Appl. Non-Class. Log., V17, P231, DOI [DOI 10.3166/JANCL.17.231-253, /10.3166/jancl.17.231-253]

[9]

Lutz C., 2006, AUTONOMOUS AGENTS MU, P137, DOI DOI 10.1145/1160633.1160657

[10]

Plaza J.A., 1989, P 4 INT S METHODOLOG, P201

← 1 2 →