Information Technology Reference
In-Depth Information
M
∩˕
abbreviates
M
∩˕
M
and
M
ↆ˕
abbreviates
M
ↆ˕
M
.Ifweuse the symbol
where
∗∈{∩,ↆ}
˕ˈ
to denote either semantics then, from
's definition,
M
∗˕
,w|=
∗
ˈ
-
M,w|=
∗
˕ˈ
i
ffM,w|=
∗
˕
and
.
The subscript
|=
∗
when its meaining is clear from the
context. A sound and complete axiomatization for
∗∈{∩,ↆ}
will be dropped from
L
PAL
w.r.t. the provided semantics
under
MNM
s can be found in [17]. The purpose of this paper is to develop tableau sys-
tems for both logics. The following proposition is a generalization of the monotonicity
of
˕
M
ↆ
ˈ
M
)tothepublic announce-
ments extensions and it will be key for providing
˕
M
ↆ ˈ
M
implies
under
MNM
s(
'srules for both intersection and
subset semantics.
Proposition 1.
Let
ˁ
i
(1
≤
i
≤
n
)
,
ʸ
j
(1
≤
j
≤
m
)
and
˕
be
L
PAL
-formulas and
M=
(
W
,˄,
V
)
be a MNM.
(i)
[
ˁ
1
]
···
[
ˁ
n
]
˕
M
ↆ
[
ʸ
1
]
···
[
ʸ
m
]
ˈ
M
implies
˕
M
∩ˁ
1
;
···
;
∩ˁ
n
ↆ ˈ
M
∩ʸ
1
;
···
;
∩ʸ
m
ˁ
1
···ˁ
n
˕
M
ↆ ʸ
1
···ʸ
m
ˈ
M
implies
˕
M
ↆˁ
1
;
···
;
ↆˁ
n
ↆ ˈ
M
ↆʸ
1
;
···
;
ↆʸ
m
(ii)
Proof.
For (i), assume
[
ˁ
1
]
···
[
ˁ
n
]
˕
M
ↆ
[
ʸ
1
]
···
[
ʸ
m
]
ˈ
M
.Nowfixany
w ∈
W
M
∩ˁ
1
;
···
;
∩ˁ
n
∈ ˄
∩ˁ
1
;
···
;
∩ˁ
n
(
with
,w |=
∩
˕
. By semantic interpretation, there is
X
w
)
˄
∩ˁ
1
;
···
;
∩ˁ
n
(
s.t.
X
ↆ ˕
M
∩ˁ
1
;
···
;
∩ˁ
n
; then, by the definition of
w
), there is
Y
∈ ˄
(
w
)s.t.
(
Y
∩ˁ
1
M
∩···∩ˁ
n
M
∩ˁ
1
;
···
;
∩ˁ
n
−
1
)
ↆ ˕
M
∩ˁ
1
;
···
;
∩ˁ
n
, i.e.,
Y
ↆ
[
ˁ
1
]
···
[
ˁ
n
]
˕
M
and hence,
∈˄
∩ʸ
1
;
···
;
∩ʸ
m
(
by assumption,
Y
ↆ
[
ʸ
1
]
···
[
ʸ
m
]
ˈ
M
.Thus,
Y
ↆ ˈ
M
∩ʸ
1
;
···
;
∩ʸ
m
for
Y
w
)so
M
∩ʸ
1
;
···
;
∩ʸ
m
,w|=
∩
ˈ
, as needed.
For (ii), assume
ˁ
1
···ˁ
n
˕
M
ↆ ʸ
1
···ʸ
m
ˈ
M
.Nowfixany
w ∈
W
with
M
ↆˁ
1
;
···
;
ↆˁ
n
∈˄
ↆˁ
1
;
···
;
ↆˁ
n
(
,w|=
ↆ
˕
. Then there is
X
w
)s.t.
X
ↆ ˕
M
ↆˁ
1
;
···
;
ↆˁ
n
and, by defi-
˄
ↆˁ
1
;
···
;
ↆˁ
n
(
nition of
w
), both
X
∈˄
(
w
)and
X
ↆ
(
ˁ
1
M
∩···∩ˁ
n
M
ↆˁ
1
;
···
;
∩ˁ
n
−
1
∩˕
M
ↆˁ
1
;
···
;
∩ˁ
n
),
i.e.,
X
ↆˁ
1
···ˁ
n
˕
M
and hence, by assumption,
X
ↆʸ
1
···ʸ
m
ˈ
M
.Thus,
X
∈
˄
ↆʸ
1
;
···
;
ↆʸ
m
(
M
ↆʸ
1
;
···
;
ↆʸ
m
w
)and
X
ↆˈ
M
ↆʸ
1
;
···
;
ↆʸ
m
so
,w|=
ↆ
ˈ
, as needed.
3
Tableaux for Non-normal Monotone (Static) Epistemic Logic
There are several works on tableau calculus of non-normal modal logic. Kripke [16]
proposed a calculus based on Kripke semantics which allow the notion of
normal world
,
and [8] constructed a uniform framework for tableau calculi for neighborhood seman-
tics employing labels for both a states and set of states. More recently, Indrzejczak [15]
avoided the label for set of states while presenting tableau calculi for several non-normal
logics over neighborhood semantics.
As a prelude to our contribution, here we recall the tableau method for non-normal
monotone modal logic of Indrzejczak [15], of which our proposal is an extension, as
well as the argument for soundness and completeness. Then we recall why the satisfia-
bility problem for non-normal monotone modal logic is NP-complete [29].
))
(
˃
:
¬˕
)
|
(
˃
:
¬ˈ
)
(
˃
:
¬
(
˕∧ˈ
(
˃
:
˕∧ˈ
)
(
˃
:
˕
)(
˃
:
ˈ
)
(
˃
:
¬¬˕
)
(
˃
:
˕
)
(
˃
:
˕
)(
˃
:
¬ˈ
)
(
˃
ne
w
:
˕
)(
˃
ne
w
:
¬ˈ
)
(
∧
)
(
¬∧
)
(
¬¬
)
(
)
Fig. 1.
Tableau rules for non-normal monotone logic [15]