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

σ : X→ X ). For a term, atom or literal M , the result of applying σ to M is de-

noted by Mσ . A substitution σ is called ground iff xσ is ground for all x

T ( Σ,

∈X . We write

{ x 1 → t 1 ,...,x n → t n } to denote a substitution σ such that x i σ = t i for 1 ≤ i ≤ n

and xσ = x for x/

∈{ x 1 ,...,x n }

.
A clause is a finite set of positive literals A and negative literals

¬ A ,where A is

L k ,where L 1 ,...,L k
are literals. For a term t we denote the set of variables occurring in t by Vars ( t ).
Respectively, we denote this set by Vars ( L ) for a literal L and Vars ( C ) for a clause

{ L 1 ,...,L k }

by L 1 ∨···∨ an atom . We also denote a clause

.
A Horn clause is a clause that contains at most one positive literal. A Horn clause

C

A ∨¬ A 1 ∨···∨¬ A k is also written as A ⇐ A 1 ∧···∧ A k . A is the head and

A 1 ∧···∧ A k is the body of this Horn clause. Again we define Vars ( A 1 ∧···∧ A k ):=

k
i =1

∪ Vars ( A i ).If k =0holds, then the body is denoted by . A negative literal within a

Horn clause is also called query .An interpretation is a set of ground atoms. A model of
a set of clauses is an interpretation, in which all clauses are satisfied. We also consider
an interpretation as a mapping from predicates to sets of ground terms, i.e., for some
interpretation

holds. For every set S of Horn clauses
there exists a unique least model, which we denote by

I we write t ∈I ( P ) iff P ( t ) ∈I

H S . H S is the set of ground

atoms which can be derived using the rule
A 1 σ...A k σ

σ is ground and A ⇐ A 1 ∧ ... ∧ A k ∈ S .

Aσ

Hence we can associate a derivation with every atom in H S .The size of this derivation

is the number of times the above rule is applied.
A term, atom or literal is called linear iff no variable occurs twice in it. A Horn
clause H

is called linear iff its head H is linear. A linear Horn clause C is called
normal iff it is of the form

⇐B

Q k ( x k ) .
This is equivalent to the definition of Nielson et al. [12]. We denote the set of all normal
Horn clauses by

P ( f ( x 1 ,...,x k )) ⇐ Q 1 ( x 1 ) ∧···∧

N

. A normal Horn clause can be considered as a transition rule in a tree
automaton. The predicates are the states of the tree automaton. Accordingly, the least
model

H S of a finite set S of normal Horn clauses maps every occurring predicate to a
regular tree language. A set S of Horn clauses is called normalizable iff there exists a
finite set S of normal Horn clauses which is equivalent to S (up to auxiliary predicates).
Two variables x and y are connected in a clause iff x = y ,where = is

the smallest equivalence relation such that the following holds: if x and y occur in the
same literal L i for i

{ L 1 ,...,L n }

,then x = y .Twoterms t 1 and t 2 are connected in a

∈{ 1 ,...,n }

clause iff there exist variables x 1 ∈ Vars ( t 1 ) and x 2 ∈ Vars ( t 2 ) such that x 1 and

x 2 are connected in

C

. Two (occurrences of) terms are called siblings in a term or literal
iff they occur as an argument of a common father. A Horn clause H

C

H 1
iff it is linear and the following statement holds: if two variables x, y occur in H and
are connected in

⇐B is called

,then x and y are siblings in H (cf. Nielson et al. [12]).
Only regular tree languages can be expressed using finite sets of

B

H 1 Horn clauses.
Nielson et al. [12] have shown this by specifying a normalization procedure, which,
given a finite set of H 1 Horn clauses, constructs an (up to auxiliary predicates) equiv-

alent finite set of normal Horn clauses. Using finite sets of linear Horn clauses we