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

are also able to encode non-regular tree languages. The least model of the finite set
S = { P ( f ( x ) ,f ( y )) ⇐ P ( x, y ) ,P ( a, a ) ⇐ } of linear Horn clauses, for instance,

is given by H S = { P ( a, a ) ,P ( f ( a ) ,f ( a )) ,P ( f ( f ( a )) ,f ( f ( a ))) ,... } . Obviously, the

set H S is not regular. Therefore, it is not possible to construct an equivalent finite set

of normal Horn clauses for every finite set of linear Horn clauses. Accordingly, it is
not the case that the normalization semi-procedure we present in the present article will
terminate for every finite set of linear Horn clauses. Nevertheless there exist meaningful
examples of finite sets of linear Horn clauses that are not finite sets of H 1 Horn clauses

which still define regular tree languages. Our method moreover can be considered as an
instantiation technique (cf. Nielsen et al. [11]).
We emphasize that we cannot expect an algorithm that terminates for every finite set
of linear Horn clauses, because the satisfiability problem for finite sets of linear Horn
clauses is undecidable Goubault-Larrecq [6].

2.2 The Normalization Semi-procedure

The goal of our normalization semi-procedure we are now going to present is to con-
struct an equivalent set of normal Horn clauses from a given set of linear Horn clauses.
Our normalization semi-procedure is a strict extension and at the same time a simplifi-
cation of the normalization procedure of Nielson et al. [12] for finite sets of H 1 Horn

clauses. The main difference is that we introduce auxiliary predicates on demand during
the normalization process instead of doing so beforehand.
In order to describe our normalization semi-procedure, we consider sets of unary
predicates as unary predicates. Additionally, we identify the set { P } with the predi-

cate P . A predicate stands for the intersection of the success sets of the

contained predicates P 1 ,...,P n . We therefore call them intersection-predicates . Con-
ceptually an intersection predicate

{ P 1 ,...,P n }

{ P 1 ,...,P n } is defined by the Horn clause

{ P 1 ,...,P n } ( X ) ⇐ P 1 ( X ) ∧···∧ P n ( X ) .

The additional power of our normalization semi-procedure relies on the fact that it intro-
duces auxiliary predicates of the form P t ,where P is a predicate and t is a term that is
built up from constants, variables, function symbols, unary predicates and a special con-
stant

. The unary predicates are used as constants. Predicates of the form P t are called
push-predicates . An example of a push-predicate is the predicate P ( f ( ) ,Q ) ,where f is
a unary function symbol and P , Q are predicates. In our normalization semi-procedure,
the term t describes the context in which the auxiliary predicate P t is introduced.
We define a relation on sets of Horn clauses. The relation represents one step
of the saturation process. If this saturation process terminates, then the set of normal
Horn clauses that are contained in the saturated set of Horn clauses is (up to auxiliary
predicates) equivalent to the initial set of Horn clauses ( soundness ). For convenience we
assume w.l.o.g. that all clauses H

in the initial set satisfy the property Vars ( H ) ⊆
Vars ( B ). This can be done w.l.o.g., because, if some variable x occurred in H but not
in

⇐B

P all ( x ) where P all is an auxiliary
predicate which accepts all terms. This property is also satisfied by all new clauses
generated by our normalization semi-procedure.

B

, then we could replace the clause with H

⇐B∧