Information Technology Reference
In-Depth Information
˃
:
L
˕
˃
-
of the form (
) with
a world symbol,
L
a list of announced formulas (
is
˕
˃
the empty list) and
survives the successive announce-
ments of the elements of
L
and afterwards it satisfies
aformula, indicating that
˕
,or
-
of the form (
˃
:
L
×
), indicating that
˃
does not survive successive announcements
of the elements of
L
.
Figure 2 shows the tableau rules for non-normal public annoucement logics. We
define the rule set for the
∩
), while the rule
∩
-semantics as all the common rules plus(
ↆ
).
set for the
ↆ
-semantics as all the common rules plus(
(
˃
:
L
p
)
(
˃
:
p
)
(
˃
:
L
¬
p
)
(
˃
:
¬
p
)
(
˃
:
L
;
˕
×
)
(
˃
:
L
¬˕
)
|
(
˃
:
L
×
)
(
ₓ
)
(
ₓ¬
)
(
×
Back
)
Common rules:
(
˃
:
L
˕∧ˈ
)
(
˃
:
L
˕
)(
˃
:
L
ˈ
)
(
˃
:
L
¬
(
˕∧ˈ
))
(
˃
:
L
¬˕
)
|
(
˃
:
L
¬ˈ
)
(
˃
:
L
¬¬˕
)
(
˃
:
L
˕
)
∧
(
¬∧
)
¬¬
(
)
(
)
(
˃
:
L
;
˕
ˈ
)
(
˃
:
L
˕
)
˃
˕
ˈ
)
(
˃
:
L
¬˕
)
|
(
˃
:
L
;
˕
ˈ
)
(
:
L
[
]
(
˃
:
L
¬
[
˕
]
ˈ
)
(
˃
:
L
;
˕
¬ˈ
)
(
Back
)
([
·
])
(
¬
[
·
])
(
˃
:
L
˕
)(
˃
:
L
¬ˈ
)
(
∩
)
For
∩
-semantics:
˃
ne
w
:
L
˕
˃
ne
w
:
L
¬ˈ
|
˃
ne
w
:
L
×
˃
ne
w
:
L
¬ˈ
(
)(
)
(
)(
)
(
˃
:
L
˕
)(
˃
:
L
¬ˈ
)
(
˃
ne
w
:
L
¬ˈ
)(
˃
ne
w
:
L
˕
)
|
(
˃
ne
w
:
L
×
)(
˃
ne
w
:
L
˕
)
(
ↆ
)
For
ↆ
-semantics:
Fig. 2.
Tableau rules for handling public announcements
Rules (
∧
), (
¬∧
)and(
¬¬
) deal with propositional reasoning.Rules (
ₓ
), (
ₓ ¬
)
¬
·
indicate that valuations do not change after a sequence of announcements. Rule (
[
])
¬
˕
ˈ
˃
¬ˈ
states that if
[
]
holds in
after a sequence of announcements
L
then
must hold
˃
˕
·
˕
ˈ
in
after the sequence of announcements
L
;
.Rule ([
]) states that if [
]
holds in
˃
after a sequence of announcements
L
, then either
˕
fails in
˃
after a sequence of
announcements
L
or else
ˈ
holds in
˃
after the sequence of announcements
L
;
˕
.Rule
(
Back
) deals with a world surviving asequence of announcements, and rule (
×
Back
)
deals with a world not surviving it.
The rule of (
∩
) is a rewriting of the first item of Proposition 1 into the rule of
tableau calculus. For simplicity, let usassume that
L
ˁ
and
L
≡ʸ
.Bytaking the
contrapositive implication of Proposition 1.(i), we obtain the following rule:
(
˃
:
ˁ
;
ˁ
˕
)(
˃
:
ʸ
¬ˈ
)
(
˃
ne
w
:
[
ˁ
][
ˁ
]
˕
)(
˃
ne
w
:
¬
[
ʸ
]
ˈ
)
≡ˁ
;
While (
˃
ne
w
:
¬
[
ʸ
]
ˈ
) generates (
˃
ne
w
:
ʸ
¬ˈ
)bytherule (
¬
[
·
]), we have two cases
ˁ
]
for expanding (
˃
ne
w
:
[
ˁ
][
˕
). First, assume that
˃
ne
w
survives after the successive
ˁ
. Then, we may add (
updates of
ˁ
and
˃
ne
w
:
ˁ
:
ˁ
˕
) to the branch. Second, sup-
ˁ
. Then, we add
pose that
˃
ne
w
does not survive after the successive updates of
ˁ
and
∩
)for
(
˃
ne
w
:
ˁ
;
ˁ
×
) to the branch. This also explains the soundness of (
∩
-semantics.
