Logic Foundation of Artificial Intelligence - Advanced Artificial Intelligence - page 70

(1) ◇ J ⊆ ◇ ϕ r, p1 and ◇ J ◇ ϕ r, p2 for each r ∈ J , 1 p 1 m r and 1 p 2 n r , and

(2) For each t § J , there must be a q 1 with 1 q 1 m t or a q 2 with 1 q 2 n t such that

◇ ϕ t, q1 or ◇ J ⊆ ◇ ϕ t, q2 . ◇ J

Lemma 2.5

(The semantic approach) J has the O -property if and only if the

following formula set is satisfiable:
{ J ϕ r,p 1 | r ∈ J and 1 p 1 m r } ∪ {¬ϕ r, p2 | r ∈ J and 1 p 2 n r }

∪ { ɂ J } ∪ { ∨ t § J mt { J nt { J

∧ ¬ϕ t,q1 } ∨ ∨ t § J ϕ t,q2 }} .

1 q 1 1 q 2

ɂ J Here

jj .
According to theorems on normal forms and either Lemma 2.4 or Lemma 2.5,
we can conclude that for any set

is the abbreviation of ∨ j ∈ J ɂ

J ⊆{1, …, k } it is decidable to examine whether

J has the O -property.

Theorem 2.10 Let ɂ be a basic formula which is represented in the disjunctive

normal form ɂ ɂ 2 ∨ ··· ∨ ɂ k , where each ɂ i (1 ± i ± k) is of the form B ϕ i,1 1 ∨

∧ ··· ∧ B ϕ i,mi ∧ ¬ B ϕ i,1 ∧ ··· ii an objective formula.

Then, for any set J ⊆ {1, …, k}, there is a decision procedure to decide whether J
has the

∧ ¬ B ϕ i,ni ∧ ϕ ii with ɂ

O -property.

Furthermore, according to Lemma 2.5 and the fact that SAT problem is
NP-completed, we can conclude that it is also a NP-completed problem to decide
whether any set } has the O -property.

With the help of ◇ -mark and O -property, we can construct a procedure to
decide the stable expansions of a basic formula.
Theorem 2.11

J ⊆{1, ···, k

Let ɂ be a basic formula which is represented in the disjunctive

normal form ɂ ɂ 2 ∨ ··· ∨ ɂ k , where each ɂ i (1 ± i ± k) is of the form B ϕ i,1 1 ∨

∧ ··· ∧ B ϕ i,mi ∧ ¬ B ϕ i,1 ∧ ··· ∧ ¬ B ϕ i,ni ∧ ɂ ii with ɂ ii an objective formula,

and let W,w be a model. Then, W,w O ɂ if and only if there exist a set J ⊆ {1, ,

···

k} which has the O -property and satisfys W= ∪ j ∈ J ◇ ɂ

jj = ◇∪ j ∈ J

ɂ

jj .