Information Technology Reference
In-Depth Information
Tableaux for Non-normal Public Announcement Logic
MinghuiMa
1
,Katsuhiko Sano
2
,Fran¸ois Schwarzentruber
3
,
and Fernando R. Velazquez-Quesada
4
1
Center for the Study of Logic and Intelligence, Southwest University, China
2
School of Information Science, Japan Advanced Institute of Science and Technology, Japan
3
ENS Rennes, Campus de Ker Lann 35170 Bruz, France
4
Grupo de L ogica, Lenguaje e Informaci on, Universidad de Sevilla, Spain
Abstract.
This paper presents a tableau calculus for two semantic interpretations
of public announcements over monotone neighbourhood models: the intersection
and the subset semantics, developed by Ma and Sano. We show that both calculi
are sound and complete with respect to their corresponding semantic interpre-
tations and, moreover, we establish that the satisfiability problem of this public
announcement extensions is NP-complete in both cases. The tableau calculi has
been implemented in Lotrecscheme.
1
Introduction
Public announcement logic (
PAL
;[7,21])studies the e
ect of the most basic com-
municative action on the knowledge of epistemic logic agents (
EL
; [12,6]), and it has
served as the basis for the study of more complex announcements [3] and other forms of
epistemic changes [27,25]. Under the standard
EL
semantic model, relational models,
PAL
relies on a natural interpretation of what the public announcement of a formula
ff
˕
˕
does: it eliminates those epistemic possibilities that do not satisfy
. Despite its sim-
plicity,
PAL
has proved to be a fruitful field for interesting research, as the characteri-
sation of successfulformulas (those that are still trueafterbeing truthfully announced:
[28,14]), the characterisation of schematic validities [13] and many others [24].
However, relational models are not the uniquestructures for interpreting
EL
for-
mulas, and recently there have been approaches that, using the so called
minimal
or
neighborhood
models [23,18,19,4], have studied not only epistemic phenomena but
also their dynamics [31,26,17,30]. The set of
EL
validities under neighborhood models
is smaller than that under relational models, so the agent's knowledgehasless'built-in'
properties, which allows a finer representation of epistemic notions and their dynamics
without resorting to 'syntactic' awareness models [5].
In [17], the authors presented two ways of updating (monotone) neighborhood mod-
els and thus of representing public announcements: one intersecting the current neigh-
borhoods with the new information (
-semantics
, already proposed in [31]), and
another preserving only those neighborhoods which are subsets of the new information
(
∩
erently, as their provided sound and com-
plete axiom systems show. The present work continues the study of such updates, first,
by extending the tableau system for monotone neighborhood models of [15] with rules
for dealing with its public announcement extensions, and second, by showing how the
satisfiability problem is NP-complete for both the intersection and the subset semantics.
ↆ
-semantics
). The two updates behave di
ff
