Information Technology Reference
In-Depth Information
3.2 Complexity
Normal modal logics as
K
and
KT
are PSPACE-complete, and negative introspection
¬
p
makes any modal logics between
K
and
S4
NP-complete [11]. Tableau
systems for such logics have been given in [10].
The satisfiability problem (deciding whether a given
p
ₒ¬
is satisfiable) for non-normal
monotone modal logic is NP-complete [29]. A known method is to build a tableau from
{
˕
(
˃
initial
:
˕
)
}
; at each step, the process adds non-deterministically a term of the form
(
˃
:
ˈ
) with
˃
is a symbol and
ˈ
is a subformula or a negation of a subformula of
˕
.
Proposition 2.
When executing thetableau method from
{
(
˃
initial
:
˕
)
}
,the number of
terms
(
˃
:
ˈ
)
thatcan be added is polynomialin thelength of
˕
.
Proof.
As
ˈ
is a subformula or a negation of a subformula of
˕
,thenumber of possible
ˈ
is linear in the size of
˕
.Thenumber of possible world symbols
˃
is polynomial
in the size of
˕
, as they are created only for pairs of the form
ˈ
1
,
¬ˈ
2
.Thus, the
2
, and hence the number of possible terms (
number of such
˃
is bounded by
|˕|
˃
:
ˈ
)
3
.
Corollary 1.
Thesatisfiability problem innon-normal monotone modallogic is NP-
complete.
is bounded by
|˕|
Proof.
NP-hardness comes from the fact that the satisfiability problem for classical propo-
sitional logic is polynomially reducible to the satisfiability problem for non-normal mono-
tone modal logic. Now let usfigure out why it is in NP. In the non-deterministic algorithm
shown below, the size of
ʘ
is polynomial in the length of
˕
(Proposition 2). Testing that
ʘ
is saturated or non-deterministically applying arule can be implemented in polynomial
time in the size of
ʘ
; then, these operations are polynomial in the length of
˕
.Asweadd
atermto
at each iteration of the
while
loop, there are at most a polynomial number of
iterations. Therefore, the tableau method can be implemented in polynomial time on a
non-deterministic machine.
ʘ
procedure
sat(
˕
)
ʘ
:
={
(
˃
initial
:
˕
)
}
while
ʘ
is not saturated
ʘ
:
=
result of the (non-deterministic) application of a rule on
ʘ
if
ʘ
is closed
then reject
accept
4
Tableaux for Non-normal Public Annoucement Logics
Tab leauxforpublic announcements for normal modal logic already appeared in [2],
where the tableau formalism needed to represent the information of accessibility rela-
tion. Since we are concerned with non-normal modal logic characterized by neighbor-
hood models, ourtableau calculus will not introduce any formalism for accessibility
relation. In this sense, our work is not a trivial generalization of [2]. For non-normal
monotone modal logic, this section adapts the tableau method of Section 3 to deal with
public announcements under both the
∩
-andthe
ↆ
-semantics. Here, terms in the tableau
rules can be either
