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

Q ( x ) and Q ( f ( x 1 ,...,x k )) ⇐ i =1 are Horn clauses P ( x ) ⇐ Q ( x i ) in S K− 1 .

Thus we have

D 1 ··· D k

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

D =

Q ( x i ) ,

P ( f ( t 1 ,...,t k ))

where the conclusion of D i is Q i ( t i ) for all i =1 ,...,k . In order to get a smaller
derivation, we substitute the subderivation D with the following smaller derivation
D 1 ··· D k

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

Q ( f ( t 1 ,...,t k )) P ( x ) ⇐

Q ( x )

P ( f ( t 1 ,...,t k ))
Case 2: The normalization step from S K− 1 to S K is an application of the inference

{C 2 }⊆ I K ⊆{C 1 , C 2 }

rule ( sp ). Thus we have ,where

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

| l ) ⇐ i∈{ 1 ,...,k|x i ∈ Vars ( t| l ) }

C 2 = P t [ ] l {x i →Q i |i =1 ,...,k} ( t Q i ( x i ) .

Case 2.1: The last inference of D is an application of C 1 . Thus D has the form

D ···

,

C 1

P ( ··· )

where the conclusion of D is P t [ ] l {x i →Q i |i =1 ,...,k} ( t ). The last inference of
the derivation D must be some application of a Horn clause from I .Nowwe
replace the sub-derivation D instead of the sub-derivation D .
Case 2.2: The last inference of D is an application of C 2 .

Case 2.2.1: There is a sub-derivation of D of the form
D b 1 ··· D b r

C 2

P t [ ] l {x i →Q i |i =1 ,...,k} ( t | l { x i → t i | i =1 ,...,k } ) D a 1 ··· D a s ,

C 1

P ( t { x i → t i | i =1 ,...,k } )

where the conclusion of the derivation D i is Q i ( t i ) for all i = i,...,k and
moreover { a 1 ,...,a s }∪{ b 1 ,...,b r } = { 1 ,...,k } , a 1 ,...,a s ,b 1 ,...,b r

are pair-wise distinct, x a 1 ,...,x a s ∈ / Vars ( t | l ),and x b 1 ,...,x b r ∈

C = P ( t ) ⇐ i =1 Vars ( t | l ). Since the Horn clause Q i ( x i ) must be

amemberof S K− 1 , we can replace the derivation D with the smaller

derivation

D 1 ··· D k

C

.

P ( t { x i → t i | i =1 ,...,k } )

Case 2.2.2: There is no sub-derivation of D of the form
D b 1 ··· D b r

C 2

P t [ ] l {x i →Q i |i =1 ,...,k} ( t | l { x i → t i | i =1 ,...,k } ) D a 1 ··· D a s ,

C 1

P ( t { x i → t i | i =1 ,...,k } )