Normalization of Linear Horn Clauses - Formal Methods: Foundations and Applications - page 250

where the conclusion of the derivation D i is Q i ( t i ) for all i = i,...,k and
moreover { a 1 ,...,a s }∪{ b 1 ,...,b r } = { 1 ,...,k } , a 1 ,...,a s ,b 1 ,...,b r

are pair-wise distinct, x a 1 ,...,x a s ∈ / Vars ( t | l ) and x b 1 ,...,x b r ∈

Vars ( t

| l ). We choose some sub-derivation D

of the form

D ···

C .

P ( t )

The Horn clause C must be from the set I . We replace the sub-derivation

D instead of the sub-derivation D .

The other cases, which are similar to those encountered for classes like H 1 , can also be

treated straightforwardly.

Whenever the normalization procedure terminates, the normal Horn clauses which
are contained in the saturated set describe the least model completely:

Lemma 2 (Completeness). Let S be a set of linear Horn clauses and S ∗ S ,where S
is saturated. Then H S∩N ( P )= H S ( P ) holds for every predicate P which occurs in S .

Proof. First of all, we define the size of a derivation. For that we define the measure
μ ( C ) of a Horn clause C as 3 m + n ,where m is the number of sub-terms occurring
in the head and n is the number of sub-terms occurring in the body. Then, the measure
μ ( D ) of a derivation D is simply the sum of the measures of the Horn clauses used
within the derivation.
For the sake of contradiction assume that t ∈H S ( P ) \H S∩N ( P ) holds, where P

occurs in S .Let D be a derivation for the atom P ( t ) of minimal measure. Within D
there exists some sub-derivation

D 1 ··· D k

D = C

P ( t )

and D 1 ,...,D k are normal derivations, i.e., only normal Horn clauses
are used within the derivations D 1 ,...,D k .

C ∈N /

such that

Case 1: C = P ( x ) ⇐ Q ( x ). In this case we have k =1and

D 1 ··· D l Q ( f ( x 1 ,...,x l )) ⇐

D 1 = Q 1 ( x 1 ) ∧···∧ Q l ( x l ) .

Q ( t )

C := P ( f ( x 1 ,...,x l )) ⇐ Since S is saturated, we have Q 1 ( x 1 ) ∧···∧ Q l ( x l ) ∈

S . Thus we can replace the sub-derivation D with the smaller derivation

D 1 ··· D l

C

.

P ( t )

Thus we have constructed a smaller derivation for P ( t ) — contradiction.