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

will not discuss these improvements in detail. Instead, we remark that our normaliza-
tion semi-procedure combines the two phases of the normalization procedure given in
[12]. Using the same arguments as in [12], we deduce that for a given finite set of

H 1
Horn clauses, our normalization procedure terminates after at most exponentially many
normalization steps:

Corollary 1. Our normalization semi-procedure normalizes a finite set of H 1 Horn

clauses in exponential time.

2.3 Instantiation

In this section we compare our techniques with instantiation as described by Nielsen
et al. [11]. Assume that S is a finite set of Horn clauses. Let us consider a Horn clause
C

≡ H ⇐B∈ S and a set { x 1 ,...,x k }⊆ Vars ( B ) of variables. If the set

I := { ( t 1 ,...,t k ) | t 1 ,...,t k ∈ T ( Σ ) , H S | = B{ x 1 → t 1 ,...,x k → t k }}

of possible values for the vector of variables ( x 1 ,...,x k ) is finite , we are able to in-
stantiate this vector of variables with all possible values. This means we can replace the
Horn clause C by the Horn clauses C{x 1 →

I ,

t 1 ,...,x k → t k } for all ( t 1 ,...,t k ) ∈

where I is some finite superset of I . We obtain a finite set S of Horn clauses that is

equivalent to S .
Thus, in some cases we can replace a Horn Clause C that does not belong to

H 1 (or
to some other syntactically defined class) by a set of Horn clauses which have fewer
occurrences of variables and thus may belong to H 1 . We refer to Nielsen et al. [11] for

a detailed explanation of this framework.

Example 2. Consider the following finite set S of linear Horn clauses:

P ( x, y ) ⇐ A ( x ) ∧ B ( y ) (11)

A ( a ) ⇐ (12)

B ( b ) ⇐ (13)

B ( h ( x )) ⇐ B ( x ) (14)

Q ( a ) ⇐ (15)

Q ( b ) ⇐ (16)

P ( f ( x ) ,g ( y )) ⇐ P ( x, y ) ∧ Q ( x ) (17)

The Horn clause (17) is not H 1 ,since x and y are connected in the body, but they are not

siblings in the head. However, the set is finite. Therefore, the variable

x in the Horn clause (17) can be instantiated, i.e., (17) can be replaced by

H S ( Q )= { a, b }

P ( f ( a ) ,g ( y )) ⇐ P ( a, y ) ∧ Q ( a ) (18)

P ( f ( b ) ,g ( y )) ⇐ P ( b, y ) ∧ Q ( b ) . (19)

By doing so, a finite set S of Horn clauses is obtained that is equivalent to S ,i.e.
H S = H S . Since all Horn clauses of S belong to the class

H 1 , now the methods of
Nielson et al. [12] or the methods of Goubault-Larrecq [7] can be applied.