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]
 
Search WWH ::




Custom Search