Information Technology Reference
In-Depth Information
Theorem 2.7
(Stable expansion) For any basic formula
ɂ
and any maximal set
of assignments W, W
ż
O
ɂ
iff the set {
ɂ
|
ɂ
is a basic formula and W
ż
B
ɂ
}
is a stable expansion of {
ɂ
}.
Corollary 2.1
has exactly as many stable expansions as there are
masimal sets of assignments where
A formula
ɂ
O
ɂ
is true.
2.8.3
Theorems on normal forms
Theorems on normal forms play important roles in the study of stable set and
stable expansion. In the following we reinspect these theorems from the point of
semantics.
Definition 2.22
For any basic formula
ɂ
, rank(
ɂ
) is inductively defined as
follows:
(1) if
is an objective formula, then rank(
) = 0;
(2) if
=
1
∧
2
, then rank(
) = Max(rank(
1
), rank(
2
));
(3) if
= ¬
, then rank(
) = rank(
ϕ
);
ϕ
(4) if
= B
ϕ
, then rank(
) = rank(
ϕ
) + 1.
Lemma 2.1
The modal operator
B
has the following properties:
(1)
B
(
B
(
))
↔
B
(
);
(2)
B
(¬
B
(
))
↔
¬
B
(
);
(3)
B
(
B
(
)
∧
ϕ
)
↔
B
(
)
∧
B
(
ϕ
);
(4)
B
(¬
B
(
)
∧
ϕ
)
↔
¬
B
(
)
∧
B
(
ϕ
);
(5)
B
(
B
)(
)
∨
ϕ
)
↔
B
(
)
∨
B
(
ϕ
);
(6)
B
(¬
B
(
)
∨
ϕ
)
↔
¬
B
(
)
∨
B
(
ϕ
).
