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

Observe that the last normalization step closes an important cycle due to the naming of
the introduced auxiliary predicates. The resulting finite set S of linear Horn clauses is
saturated and contains the following normal Horn clauses:

P ( x 1 ,x 2 ) ⇐ Q ( x 1 ) ∧ R ( x 2 ) Q ( a ) ⇐

R ( b ) ⇐ R ( g ( x )) ⇐ R ( x )

P ( x, x 2 ) ⇐ P ( ,R ) ( x ) ∧ R ( x 2 ) P ( ,R ) ( f ( x 1 )) ⇐ Q ( x 1 )

P ( ,R ) ( f ( x 1 )) ⇐ P ( ,R ) ( x 1 )

The set of these normal Horn clauses is (up to auxiliary predicates) equivalent to the
initial set of linear Horn clauses. In particular, we have

H S ∩N ( P )= { ( f i ( a ) ,g j ( b )) | i, j ∈ N } = H S ( P ) .

Note that this result cannot be obtained by using the instantiation techniques of Nielsen
et al. [11].

The set of derivable facts is (up to auxiliary predicates) preserved by executing nor-
malization steps:

Lemma 1 (Soundness). Let S be a set of linear Horn clauses and S ∗ S .Then
H S ( P )= H S ( P ) holds for every predicate P which occurs in S .

S M = S .Weset I K := S K \ Proof. Let us fix some sequence S = S 0 ··· S K− 1

for all K =1 ,...,M ,and I := S \ S . We define a size function Size which maps a

derivation in S

M

to an element from N by:

Size D 1 ···

:= Size ( C )+ i =1 Size ( D i )
Size ( C ):= ( δ 1 j ,...,δ Mj )

D k

C

A

if C∈ I j

(0 ,..., 0) otherwise

Here, δ denotes the Kronecker-Delta, i.e., δ ij equals 1 if i = j and 0 otherwise.
The elements of

M are ordered lexicographically with reversed significance, i.e.,
( a 1 ,...,a M ) < ( b 1 ,...,b M ) holds iff there exists some j

N

such that
a j <b j and a i = b i for all i>j holds. Note that the following holds: If we re-
place a subderivation of a derivation with a smaller derivation, then the derivation itself
gets smaller. Furthermore, if Size ( D )=(0 ,..., 0) holds for a derivation D , then only
clauses from S are used in D .
Let D be a derivation for a ground atom P ( t ),where P is a predicate from S and
Size ( D ) > (0 ,..., 0) holds. It is sufficient to show, that there exists a derivation D for
P ( t ) with Size ( D ) < Size ( D ).
There must be a subderivation D

∈{ 1 ,...,M }

of D , where the last inference is an application of

a Horn clause from I K for some K ∈{ 1 ,...,M } .

Case 1: The normalization step from S K− 1 to S K is an application of the inference

rule ( cp ). Let P ( f ( x 1 ,...,x k )) ⇐ i =1 Q ( x i ) be the Horn clause in I K .There