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

In order to apply the rule ( elim ) or the rule ( sp ), we have to check, whether or not
H S∩N ( Q ) holds. This means, we have to check emptiness for tree automata.

This can be done in polynomial time. During the execution of our normalization semi-
procedure, the emptiness-information can be computed on the fly. This means: For each
predicate P , we maintain the information, whether or not

= ∅

H S∩N ( P ) = ∅

holds. When-

ever we add a normal Horn clause, we update this information.
The substantial difference between our normalization semi-procedure and the nor-
malization procedure of Nielson et al. [12] is the rule ( sp ).Therule( sp ) dispenses with
the need of the pre-processing phase as described by Nielson et al. [12] or by Goubault-
Larrecq [7]. The pre-processing phases of Nielson et al. [12] and Goubault-Larrecq
[7] essentially decompose complex heads of Horn clauses P ( t ) ⇐B

through the in-
troduction of auxiliary predicates. At the end of these pre-processing phases all heads
are of the form P ( x 1 ,...,x k ) or P ( f ( x 1 ,...,x k )). The Horn clause P ( f ( x ) ,y ) ⇐
Q 1 ( x ) ∧ Q 2 ( y ), for instance, is replaced by the Horn clauses P ( x, y ) ⇐ Q ( x ) ∧

Q 2 ( y ) ,Q ( f ( x )) ⇐ Q 1 ( x ),where Q is a fresh auxiliary predicate. Note that this

step is done by the rule ( sp ). However, the Horn-clause P ( f ( x ) ,y ) ⇐

Q ( x, y ) —

which is not H 1 — cannot be replaced by (up to auxiliary predicates) equivalent Horn-

clauses whose heads are of the form P ( x 1 ,...,x k ) or P ( f ( x 1 ,...,x k )) during a pre-
processing phase, since the variables x and y are connected in the body. Here, the obser-
vation is that connection between x and y will be eliminated during the normalization
process. Therefore we postpone the decomposition of complex heads until the connec-
tion between the variables in the bodies are eliminated by the normalization process.
The rule ( sp ) does this together with a clever naming of the introduced auxiliary pred-
icates (the push-predicates). In consequence, using our new inference rules, we can
normalize finite sets of linear Horn clauses that can neither be solved through the nor-
malization procedure of Nielson et al. [12] nor through the ordered resolution procedure
of Goubault-Larrecq [7].

Example 1. We consider the following finite set S of linear Horn clauses:

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

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

Q ( a ) ⇐ (3)

R ( b ) ⇐ (4)

R ( g ( x )) ⇐ R ( x ) (5)

H S ( P )= { ( f i ( a ) ,g j ( b ))

We h ave | i, j ∈ N } . Our normalization semi-procedure

performs the following steps:

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

( sp )(6) : P ( x, x 2 ) ⇐ P ( ,R ) ( x ) ∧ R ( x 2 ) (7)

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

( cut )(1)(7) : P ( f ( x 1 ) ,x 2 ) ⇐ P ( ,R ) ( x 1 ) ∧ R ( x 2 ) (9)

( sp )(9) : P ( ,R ) ( f ( x 1 )) ⇐ P ( ,R ) ( x 1 ) (10)