Information Technology Reference
In-Depth Information
˃
:
L
γ
∈ ʘ
The first conjunct is the assumption. For the second conjunct, suppose (
)
;
M
ʘ
,˃
|=ˁ
1
···ˁ
n
γ
we show that
, i.e.,
M
ʘ
,˃
|=ˁ
1
, ...,
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
−
1
,˃
|=ˁ
n
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
,˃
|=γ.
(
and
(
˃
:
L
γ
These can be derived from (
)
∈ ʘ
,therule (
Back
)andinduction hypothesis.
M
ʘ
,˃
|=ˁ
1
···ˁ
n
γ
Therefore,
,asrequired.
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
For (ii), assume (
˃
:
L
¬γ
)
∈ ʘ
; we show that (
,˃ |= γ
,i.e.,
ˁ
1
···ˁ
n
γ
M
˄
ʘ
(
ces to show that, for all
L
and all
˃
). It su
˕
,
{˃
∈
W
ʘ
|
˃
:
L
˕
(
˃
:
L
˕
)
∈ʘ
implies
(
)
∈ʘ} ˁ
1
···ˁ
n
γ
M
ʘ
.
Thus, take any
L
and
˕
such that (
˃
:
L
˕
)
∈ ʘ
.Since(
˃
:
L
˕
)
,
(
˃
:
L
¬γ
)
∈ ʘ
,
ↆ
) imply, for some fresh
ʘ
'ssaturatedness and rule (
˃
ne
w
, either
(
˃
ne
w
:
L
¬γ
)
,
(
˃
ne
w
:
L
˕
)
∈ʘ
or (
˃
ne
w
:
L
×
)
,
(
˃
ne
w
:
L
˕
)
∈ʘ
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
,
In either case, it follows from induction hypothesis that either
˃
ne
w
is not in (
M
ʘ
)
ↆˁ
1
;
···
;
ↆˁ
n
M
ʘ
,˃
ne
w
|=ˁ
1
···ˁ
n
γ
or else (
,˃
ne
w
|=γ
, which is equivalent with
.This
{˃
∈
W
ʘ
|
˃
:
L
˕
finishes establishing our goal;
(
)
∈ʘ} ˁ
1
···ˁ
n
γ
M
ʘ
.
Theorem 6.
Given any formula
˕
,ifthere is an open saturated tableau for
(
˃
initial
:
˕
)
,
then
˕
is satisfiable in theclass of all MNMs for subset semantics.
Proof.
Similar to Theorem 5, using Lemma 6 instead.
4.3
Termination and Complexity
Thesameargument works for both semantics. In order to check
˕
's satisfiability, start
the tableau method from the set of terms
˃
initial
is the initial sym-
bol. At each step, add non-deterministically at least one term of the form (
{
(
˃
initial
:
˕
)
}
where
˃
:
L
∗
)
where
˃
is a symbol,
L
is a list of subformulas or negation subformulas of
˕
and
∗
is a
subformula or a negation of a subformula of
˕
or the symbol
×
.
Proposition 3.
When executing thetableau method from
{
(
˃
initial
:
˕
)
}
,the number of
terms
{
(
˃
:
L
∗
)
}
thatcan be added is polynomialin thelength of
˕
.
Proof.
As
∗
is a subformula or a negation of a subformula of
˕
or the symbol
×
,the
∗
˕
number of possible
is linear in the size of
.Thenumber of possible
L
is linear in
˕
ˈ
˕
the size of
since each entry corresponds to an occurrence of an operator [
]in
.
˃
˕
˃
The number of possible
is polynomial in the size of
since new world symbols
are
created for 4-tuple of subformulas of the form
ˈ
1
,
¬ˈ
2
.Thus, the number of possible
terms (
˃
:
ˈ
)isbounded by a polynomial in
|˕|
.
Corollary 2.
Thesatisfiability problem innon-normal monotonepublic announcement
logic is NP-complete.
Proof.
The proof is similar to the proof of Corollary 1 except that we use Proposition
3 instead of Proposition 2 and that we start with
ʘ
:
= {
(
˃
initial
:
˕
)
}
instead of
ʘ
:
=
{
(
˃
initial
:
˕
)
}
.
