211
Logic Programming and Artificial Neural Networks
of the A
r
i,j (2) in Step (2)) as follows.
A
1
m(i,1,1)
i,1 (2) ← A
1
i,1,1 (3), . . . , A i,1,1 (3)
m(i,1,2)
A
2
i,1 (2) ← A
1
i,1,2 (3), . . . , A i,1,2 (3)
.
.
.
.
. ←
.
m(i,1) (2) ←
1
(3)
m(i,1,m(i,1))
A i,1
A i,1,m(i,1) , . . . , A i,1,m(i,1)
(3)
1
m(i,2,1)
A i,2 (2) ← A
1
i,2,1 (3), . . . , A i,2,1 (3)
m(i,2,2)
A
2
1
i,2 (2) ← A i,2,2 (3), . . . , A i,2,2 (3)
.
.
.
.
. ←
.
m(i,2)
m(i,2,m(i,2))
A i,
(2) ← A
1
2
i,2,m(i,2) (3), . . . , A i,2,m(i,2) (3)
.
.
.
.
. ←
.
1
(2) ←
1
(3)
m(i,m(i),1)
A i,m(i)
A i,m(i),1 , . . . , A i,m(i),1 (3)
2
(2) ←
1
(3)
m(i,m(i),2)
A i,m(i)
A i,m(i),2 , . . . , A i,m(i),2 (3)
.
.
.
.
.
.
←
m(i,m(i))
m(i,m(i),m(i,m(i)))
A
(2) ← A
1
(3), . . . , A
(3),
i,m(i)
i,m(i),m(i,m(i))
i,m(i),m(i,m(i))
where each atom in each body belongs to T P ↑ (k n − 3).
Note that at each stage in this process we select a ground clause in which
the head of the clause does not occur in the body by means of the claim
established earlier.
This process terminates producing unit clauses in its last step. Let P i,n
denote the (finite) subset of ground(P ) consisting of all the clauses which
result; it is clear that T Pi,n ↑ k n consists of the heads of all the clauses in
P i,n . We carry out this construction for i = 1, . . . , m to obtain programs
P 1,n , . . . , P m,n such that, for i = 1, . . . , m, T Pi,n (T Pi,n ↑ k n ) = T Pi,n ↑ k n
(indeed, T Pi,n ↑ k n is the least fixed point of T Pi,n by Kleene’s theorem, Theorem 1.1.9), A i ∈ T Pi,n ↑ k n , and T Pi,n ↑ r ⊆ T P ↑ r ⊆ I for all r ∈ N. Let
P n denote the program P 1,n ∪ . . . ∪ P m,n . Then P n is a finite subprogram
of ground(P ), and T Pi,n ↑ k n ⊆ T P n ↑ k n ⊆ T P ↑ k n ⊆ I for i = 1, . . . , m.
Furthermore, A 1 , . . . , A m ∈ T ↑ k n , and T ↑ k n is the least fixed point I n
P n
P n
of T .
P n
This completes the construction of the program P n .
7.5.11 Example We illustrate the process just described with k = k n = 3.
Suppose that A 1 ∈ T P ↑ 3 = T P (T P ↑ 2). Then there is a ground clause A 1 ←
B 1 , B 2 , say, with B 1 , B 2 ∈ T P ↑ 2 = T P (T P ↑ 1). Therefore, there exist ground
clauses B 1 ← C 1 , C 2 , C 3 and B 2 ←, say, with C 1 , C 2 , C 3 ∈ T P ↑ 1 = T P (∅).
Logic Programming and Artificial Neural Networks
of the A
r
i,j (2) in Step (2)) as follows.
A
1
m(i,1,1)
i,1 (2) ← A
1
i,1,1 (3), . . . , A i,1,1 (3)
m(i,1,2)
A
2
i,1 (2) ← A
1
i,1,2 (3), . . . , A i,1,2 (3)
.
.
.
.
. ←
.
m(i,1) (2) ←
1
(3)
m(i,1,m(i,1))
A i,1
A i,1,m(i,1) , . . . , A i,1,m(i,1)
(3)
1
m(i,2,1)
A i,2 (2) ← A
1
i,2,1 (3), . . . , A i,2,1 (3)
m(i,2,2)
A
2
1
i,2 (2) ← A i,2,2 (3), . . . , A i,2,2 (3)
.
.
.
.
. ←
.
m(i,2)
m(i,2,m(i,2))
A i,
(2) ← A
1
2
i,2,m(i,2) (3), . . . , A i,2,m(i,2) (3)
.
.
.
.
. ←
.
1
(2) ←
1
(3)
m(i,m(i),1)
A i,m(i)
A i,m(i),1 , . . . , A i,m(i),1 (3)
2
(2) ←
1
(3)
m(i,m(i),2)
A i,m(i)
A i,m(i),2 , . . . , A i,m(i),2 (3)
.
.
.
.
.
.
←
m(i,m(i))
m(i,m(i),m(i,m(i)))
A
(2) ← A
1
(3), . . . , A
(3),
i,m(i)
i,m(i),m(i,m(i))
i,m(i),m(i,m(i))
where each atom in each body belongs to T P ↑ (k n − 3).
Note that at each stage in this process we select a ground clause in which
the head of the clause does not occur in the body by means of the claim
established earlier.
This process terminates producing unit clauses in its last step. Let P i,n
denote the (finite) subset of ground(P ) consisting of all the clauses which
result; it is clear that T Pi,n ↑ k n consists of the heads of all the clauses in
P i,n . We carry out this construction for i = 1, . . . , m to obtain programs
P 1,n , . . . , P m,n such that, for i = 1, . . . , m, T Pi,n (T Pi,n ↑ k n ) = T Pi,n ↑ k n
(indeed, T Pi,n ↑ k n is the least fixed point of T Pi,n by Kleene’s theorem, Theorem 1.1.9), A i ∈ T Pi,n ↑ k n , and T Pi,n ↑ r ⊆ T P ↑ r ⊆ I for all r ∈ N. Let
P n denote the program P 1,n ∪ . . . ∪ P m,n . Then P n is a finite subprogram
of ground(P ), and T Pi,n ↑ k n ⊆ T P n ↑ k n ⊆ T P ↑ k n ⊆ I for i = 1, . . . , m.
Furthermore, A 1 , . . . , A m ∈ T ↑ k n , and T ↑ k n is the least fixed point I n
P n
P n
of T .
P n
This completes the construction of the program P n .
7.5.11 Example We illustrate the process just described with k = k n = 3.
Suppose that A 1 ∈ T P ↑ 3 = T P (T P ↑ 2). Then there is a ground clause A 1 ←
B 1 , B 2 , say, with B 1 , B 2 ∈ T P ↑ 2 = T P (T P ↑ 1). Therefore, there exist ground
clauses B 1 ← C 1 , C 2 , C 3 and B 2 ←, say, with C 1 , C 2 , C 3 ∈ T P ↑ 1 = T P (∅).