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

In the following x j are mutually distinct variables. The relation over sets of Horn
clauses is specified by an inference system. The inference rules are of the form

P 1 ··· P m

C 1 ···

,

C n

where P 1 ,...,P m are the premises and C 1 ,...,C n are the conclusions. The relation
is defined as follows: SS ∪{ C 1 ,...,C n } iff the inference rule

P 1 ··· P m

C 1 ··· C n

is a member of the inference system, P 1 ,...,P m ∈ S ,and { C 1 ,...,C n } S .Aset

S : SS . Our inference system is defined S of Horn clauses is called saturated iff

through the following inference rules:

Q ( f ( x 1 ,...,x k )) ⇐ i =1

P ( x ) ⇐ Q ( x ) Q i ( x i ) ( cp )

P ( f ( x 1 ,...,x k )) ⇐ i =1 Q i ( x i )

P ( t ) ⇐ i =1

Q i ( x i )

( sp )

P t [ ] l {x i →Q i |i =1 ,...,k} ( x ) ∧ i∈{ 1 ,...,k|x i ∈ Vars ( t| l ) }

P ( t [ x ] l ) ⇐ Q i ( x i )

| l ) ⇐ i∈{ 1 ,...,k|x i ∈ Vars ( t| l ) } P t [ ] l {x i →Q i |i =1 ,...,k} ( t Q i ( x i )

Here, l is a non-root position in t , t | l is not a variable, { x 1 ,...,x k }⊆ Vars ( t ),

x/ H S∩N ( Q i ) = ∅

means that there exists a term which satisfies the predicate Q i in the least model of the
normal Horn clauses contained in S .

∈ Vars ( t ),and H S∩N ( Q i ) = ∅ for all i =1 ,...,k . Recall that

Q ( f ( x 1 ,...,x k )) ⇐ i =1

H ⇐B∧ Q ( f ( t 1 ,...,t k )) Q i ( x i ) ( cut )

⇐B∧ i =1

H Q i ( t i )

⇐B∧ i =1 H Q i ( x )

( cap1 )

⇐B∧ ( i =1

H Q i )( x )

Here, k> 1,and x/

∈ Vars ( B ).

i =1 ,...,n

P i } ( f ( x 1 ,...,x k )) ⇐ j =1 { Q i,j ( x j ) H ⇐B∧{ P 1 ,...,P n } ( x ) ( cap2 ),

P 1 ,...,P n } ( f ( x 1 ,...,x k )) ⇐ j =1 ,...,k ( Q 1 ,j ∪···∪

{ Q n,j )( x j )

Here, n> 1,and x/ ∈ Vars ( B ).

H ⇐B∧ Q ( x )

( elim )

H ⇐B

Here, H S∩N ( Q ) = ∅ ,and x/ ∈ Vars ( H ) ∪ Vars ( B ).