An Extension of Unification to Substitution with an Application to Automatic Theorem Proving

I. Introduction

In I 51 ROBINSON introduced resolution theorem proving. He defines the notion of unifiability of expressions as follows: two expressions are called unifiable if we can find a substitution such that by applying that substitution to the expressions the expressions become equal. In §2 thedefinitions, the unification algorithm and the unification theorem are reviewed. In §3 we extend the notion of unifi­ ability to substitutions. Two substitutions are railed unifiable if we can find a substitution such that if we can compute the composition of the orig­ inal substitutions with this substitution the re­ sulting substitutions become equal in the !'et the­ oretical sense. Some theorems connecting unifiabi·­ lity of expressions and unifiability of substitu­ tions are presented. Furthermore, an algorithm for computing the unifier of substitutions is described. Applications of the notion of unifiability of sub­ stitutions to resolution theorem proving problems such as and-or tree representation, connection graphs r 3,41 and the structure sharing way of re­ presenting clauses I 1·1 are dealt with in §4.

2. The Unification of Expressions

Definitions

The following definitions are taken from L5l:

A t ePm is either a variable or a string of sym­ bols consisting of a function symbol of degree n <: 0 followed by n terms.

An expression is either a term or a string of symbols consisting of a predicate symbol of degree n ~ 0 followed by n terms.

A substitution component is any construct of the form v ~ t where v is a variable and t is a term different from v; v is called the variable of the substitution component v -· t and t is called the t erm (Hence v ~ v is not a substitution compo­ nent for any variable v).

A substi tution is a finite (possibly empty) set of substitution components with distinct left­ hand sides. Therefore in a substitution

(vi 'LJ, v2-> t2····· vk-+ tk} the order of the consti­ tuent components is immaterial. Substitutions are denoted by lower case greek letters, r is used to denote the empty substitution.

* This work was supported by the Mathematisch Centrum under number IW 24/74.

In the following variables will be denoted by strings commencing with v,w,x,y,z; constants or nullary functions by a,b,c,d,e and strings commen­ cing with f,g,h denote n-ary functions with n > I.

Let E be a finite string of symbols and A = (vi-> til~=l be a substitution. The instanLiaLion of E by A is the operation of simultaneously re­ placing each occurrence of vi in E by an occurrence of the term ti for all i, I :s i ~ k. The resulting string Ee is called the instance of E by 0. If Cis a set of strings and e a substitution then the in­ stance of C bye is defined by ce z {EeJE<Cl.

Let 9 = (vi-+ til~=l and A be substitutions. The com­ position of 9 and A is the substitution O' u A 1 where 9' consists of the components vi -+ tiA such that tjA ; vi, I s i s k and A' consists of the sub­ stitution components of A whose left-hand sides are not left-hand sides of 9.

It is easily verified that ce = Oc = 0 for all sub­ stitutions e . Similarly, composition of substitu­ tions is associative, i.e. (S A )~= 9 (Ap) and there­ fore we may omit the parentheses.

(Hint: for any expression E and a composition of substitutions o = 9A; Eo is the string E9A, that is, the instance of Ee by A).

We now summarize some properties of the composition

of substitutions which we need in the sequel. (E is an expression and o,~,A are substitutions.)

I. (Eo) A = E (oA) for all strings E and all subst i­ tutions o ,A.

1. o = A iff Eo = EA for all strings E.
2. (oA)~ · o(A~) for all substitutions o,A,~.
3. (AuB)A = AA u ·BA for all sets of strings A,B and all substitutions A. Note that the composition of substitutions is not commutative OA ; AO.

The disagreement set of a non-empty set of expres­ sions A consists of the set of well-formed subex­ pressions extracted from the e:-:pressions in A by deleting the initial parts which are common to all expressions in A.

UNIFIER. Let A be a set of expressions and e be a substitution; e is said to unify A (or to be a uni ­ f ier of A) if AS is a singleton. A set of expres­ sions which has a unifier is said to be unifiable.

MOST GENERAL UNIFIER. A unifier 9 of a set of ex­ pressions A is called a most general unifier of A if for all unifiers o of A there exists a substi­ tution A such that o = OA . If A has a unifier then there exists always a most general unifier e; AO then is called the most general instance of A. (The most general unifier of A is unique up to iso­ morphisms.)

The Algorithm and the Unification Theorem

The unification algorithm and theorem are quoted from the ROBINSON [ 51. The Unificat i.;n a lgorithm computes the most general unifier of A, where A is a finite non-empty set of expressions:

~ ; oa: = < (the empty substitution); k: = 0;

Step II : If Aok is a singleton stop: ok is the most general unifier of A.

Step III: Compute the disagreement set of Aok; or­ der this set such that the variables are in front, the rest of the ordering being immaterial.

If vk and uk are the two earliest elements of the disagreement set and vk is a variable that does not occur in uk then ok+l := ok. {vk~uk}; k :· k+l; go to step 2 otherwise stop then A is not unifiable.

UNIFICATION THEOREM. Let A be a non-empty finite set of expressions. If A is unifiab~e then there exists a most general unifier a of A which is com­ ruted by the unification algorithm.

During the computation of a deduction in auto­ matic theorem proving a great amount of unification computations has to be performed. The implementa­ tion of the unification algorithm can be done much more efficient than a straightaway implemen­ tation; See [6, 2 and 7].

J. An Extension of Unification to Substitutions

Definitions

Substitution unifier. Let 0 = {Oi}~=l be a set of substitutions and o a substitution; a is said to unify 0 or to be a unifier of 0 if eia = P. i+JO for all I ~ i < k. A set of substitutions which has a unifier is said to be unifiable or to be compatible. (By equality of substitutions is meant the set the­ oretical equality of the ordered pairs).

Instantiation. If o1 and 82 are substitutions then the composition o 1 e 2 is called an instance of e 1 .

Most genera~ unifier. A unifier a of a set of sub­ stitutions 0 = {OiJ1=l is called a most general unifier if for all unifiers 1 of 0 there exists a substitution A such that 1 = OA; the instance o 1 a is called the most general instance of 0.

Norma~ form. A substitution e = {vi~til~. 1 is in normal form if for all i,j: I ~ i, j ~ k, vi does not occur in tj.

Note

1. By definition it holds that all vi's in a sub­ stitution are different.
2. The most general unifier of expressions comput­ ed by the unification algorithm as quoted in 2.2 is in normal form.
3. The most general instance of a set of substitu­ tions {Oilt. 1 is sometimes also denoted by BJ*02· ··· ·ek; this operation is commutative and associative.

A substitution component v ~ t is called circu~ar if v occurs in t.

A set of substitutions 0 z {e.}~=) is called con­ tradictory if there are two s~bst1tutions e 1, em in 0 such that there is a substitution component Vj ~ tj 1 in e 1 and a substitution component Vj ~ tjm in Om such that vj 1 = Vjm and the terms tj 1 and tjm are not unifiable.

Algorithms and Theorems

We now give the algorithm to compute the most general unifier o of a set of substitutions {lli li=J'

We assume that in each substitution of a set of substitutions the substitution-components are or­ dered according to a fixed enumeration of all vari­ ables and there are no circular components.

Substitution Unification Algorithm.

~ k:= 0; 0 := (, Step II : Compute Pe. ok~~=l; delete components of the form v ~ v from 'BiOkl?=J· If there is a circu­ lar substitution component in one of the substitu­ tions eiok then there is no unifier and the algorithm halts. If {eioklY=I is a singleton then ok is a most general unifier and the algorithm halts. In all other cases eoto step J.

Step III: Take the first substitution component from all eiok; if they are all equal then take next ones otherwise take from this set those substitution components where the variables are first in the above mentioned enumeration on the variables, the resulting set is, say, lv~tjlT=I· We now distin­ guish three cases.

Case I : m = I. Then: k := k+l; ok := oK_ 1 . lv~tl}; goto step 2.

Case II : The set contains substitution components that come from some but not all of the sets {eiok}~=J· If the set {v-·tjlT=I is contradictory, then stop: not unifiable otherwise let A be the most general unifier of {tjlj. 1 then k :· k+l;

ok'" Ok-1· lv~t 1 l A; goto step 2.

Case III: The set contains substitution components that come from all Biok. If the set {v+t·lT·I is contradictory then halt: not unifiable olherwise let A be the most general unifier of ltjlf·l then k := k+l; ok ;z ok-J·A; goto step 2.

Examples

I. el - {x->t, y->a}; 82. {x-·f(y), z~f(y)}; BJ · lx~z, t~z, s->b}. Ordering x,y,z,t,s. k- 0: oo .. (, k · J; X-> t, X-> f(y), X-> z. compute m.g.u. of {t,f(y),z}: t ~ f(y), z-> f(y) OJ · {t~f(y), z~f(y)} BJOJ · {x->f(y), y->a, z->f(y), t->f(y)} 8201 · {x->f(y), z->f(y), t->f(y)} BJOJ · {x->f(y), z->f(y), t->f(y), s->b} 02 = OJ.{y->a} · {t->f(a), z··f(a), y->a} OJ02 = 8202 = {x->f(a), y->a, z->f(a), t->f(a)} 8Ja 2 = {x->f(a), y->a, z->f(a), t~f(a), s->b} OJ · o2.!s~bl · {t~f(a), z~f(a), y~a, s->b} OJ is the most general unifier of {BJ,02,0Jl

1. e 1 {x->y, y->f(a)}; e2 · {x->f(a), y->f(a)} OJ · {y->f(a)} is the most general unifier.
2. OJ · {x->y, y->f(a)}; 82 · {x->b, y~f(a)} a 1 · {y->b} is the most general unifier and 82 is is the most general instance.
3. e1 · {x->y}; e2 · {x->b, y->f(a)l a 1 · {y->b} OJOJ · {x->b, y->b};e2a 1·{x->b, y->f(a)l because {y->b} and {y->f(a)} are contradictory, 81 and 82 are not unifiable. (since b is not variable)

Remarks

1. The most general unifier of a set of substitu­ tions as computed by the above algorithm is al­ ways in normal form.
2. The most general instance of a set of substitu­ tions is not always a unifier of the substitu­ tions: example J: e 2 · {x->b, y->f(a)} is themost

general instance but Ot 02 · {x+f(a), y-·f(a)l '1'0202.

To compute the most general unifier of expressions we can also use the algorithm for computing the m.g.u. of substitutions if we consider the dis­ agreement set to be substitutions and look at the class of disagreement sets. The class of <lisagree­ ment sets of a nonempty set of expressions A con­ sists of the class of sets of well-formed subex­ pressions from the expressions in A by deleting the parts which are common to all expressions in A (scanning starts from the left).

Example

{R(x,y), R(g(f(x,y)), h(b)), R(a,t) ) the disagreement sets are: {x,g(f(x,y)),a} and {y,h(b) ,t}.

Algo~ithm 2 to make a set of substitutions out of a disagreement set of a set of ~xpressions if possible.

~ : If the disagreement set does not contain any variable then halt: there is no unifier. Step II: Choose one of the variables from the dis­ agreement set le 1, ... ,en} say ei and make the fol­ lowing set of (n-1) substitutions

ler·e 1J ··· ler·ci-ll {ei-+ei+l l ... {ei-+en}. If there is any substitution component circular in this set then halt: there is no unifier.

THEOREM I. Let 0 · {ailY-t be a non-empty set of substitutions. If 0 is unifiable then the~e exists a most gene~al unifie~ o of 0 and o is determined by the substitution unification algo~thm. The proof goes similarly to that of the unification theorem.

Example

at · {x+f(y), z-+al;a ·.. · {x-+f(g(s)), t-+b}

1 · {y-+g(a), z-+a, t-+b, u-+g(a), s-+a} is a unifier.

o 0 · c; >. 0 · 1 o1 2 {y-+g(s)); >. 1 · {t--b, z-+a, u-+g(a), s-·al o2 · {y-+g(s), z-+a}; >. 2 · {t-+b, u-+g(a), s-+a}

o3 · m.g.u. · {y+g(s), z-+a, t-+b}; >.3 · {u-+g(a),s+a}

THEOREM 2. Given a unifiable set of substitutions {ailY21 such t hat ei is in normal form fo~ all i. The most gene~al instance of {ai}~21 is also auni­ fie~ of {Oily. 1·

PROOF. Let the most general unifier of { a il~. 1 be o then a 1o 2 ··· = Ono is the most general in­ stance. Because of the normal form of the substi­ tutions ei. Oi · ai holds. Because of the associa­ tivity of the composition of substitutions we have: OiOio = atui o) and therefore o1e 1o = 02a2o = 02a 1o. Hence, a 1 o is a unifier. 0

THEOREM 3. Fo~ a given set of exp~essions which is unifiable we can compute the most gene~al unifie~ also by applying the substitution unification al­ go~thm on the set of substitutions formed by al­ go~thm 2 from the disag~eement sets. The1! the m.g.u. of the exp~essions is the most gene~al in­ stance of these substitutions.

(Substitutions from the second algorithm are in normal form since every substitution consists of but one substitution somponent)

The proof proceeds in two steps: first we prove that unif.iabi l i ty occurs in the same circumstances; secondly we can prove that we get the same unifier up to isomorphisms.

Example

Are P(y,f(z),z) and P(x,x,t) unifiable? Disagreement sets: {y,x}, {f(z),x} {z,tl; corre­ sponding set of subsitutions 0 = {{y-+x , ~·f(z)}, { z-+t}}.

Ordering of variables: x,y,z,t.

OJ {x-+f(z)}; aol = {{u-+f(z),y-+f(z)}, {x-+f(z)}, {x+f(z) ,z-+t} ).

02 {x-+ f(z), y-+f(z)}

03 m.g.u. = {x-+f(t), y-·f(t), z·t) . nn 3 2 ({x·f(t), y-+f(t), z->t}l.

Some Theorems Relating the Different Unifications

THEOREM 4. Given a set of exp~essions {Ei}9. 1 with a most gene~al unifie~ a then fo~ a set of 1 n sub­ stitutions {ai}Y=t the J~llowing holds. The set of instances {Eiai}Y=t is unifiable if the set of sub­ stitutions {a} u {a~}~=J is unifiable. The most gene~al unifie~ a OJ \a} u {ai}~=l is also a uni­ fie~ of {Eiai}?-t·

PROOF. If {e ) u {ai}y. 1 is unifiable then there exists a substitution a the most general unifier, such that eo · eJo · .. . · Ono ; a is the most general unifier of 'EilY-t so EtO · . · · · Ena also E1ao · = ... " Enao; replacing Go by respectively ela, ..· , ana gives EJalo · · Enano which means that a is a unif1er of the set {Ei0i}~2)· 0

Remark

The computed unifier is not necessarily the most general one because variables which occur in Ei can be deleted by substituion a. ; therefore they do not occur in the computed unifi~r. This is one of the reasons that the converse of the theorem does not hold in general.

Counterexamples

I. {P(x), P(a)} unifiable 0 = {x-+a}. Let e 1 · E and e2 = {x-+b} then {Ei0i}y. 1 · {P(x), P(a)} unifiable but OJ, 82 and e are not unifiable.

2. (P(x,y), P(y,t)} unifiable e = {x-+t, y-+t}. Let 81 = {y-+a} and a2 = {y-+c} then {EiOilY. 1 · {P(x,a), P(c, t) l unifiable but e 1, e 2 and e are not unifiable.

However, the converse theorem holds if we restrict the substitutions Oi to variables that occur in Ei and if the expressions Ei do not have any v;J.ri<~bles in common.

THEOREM 5. Let {E\}9. 1 be a set of exp~essions which have no va~~atles in common and ~e unifiable with a most gene~al unifie~ a. Let {Oi}9. 1 be a set of substi t utions such that a va~iable oacu~ing in ei does not occu~ in ej, I s i, j s nand ai has as left-hand sides of its components only va~iables occu~ing in Ei. If the set of exp~essions {E.a.}9 21 is unifi able then the set of substitut ions 1 1 1 {a} u {Ci}r=l is unifiable .

The proof proceeds by contradiction along the dif­ ferent steps of the substitution unification al­ gorithm.

Example

Given E1 = P(y,f(z),z) and E-~ = P(x,x,t) then the most general unifier of Et and E2 is o ~ {x+f(t), y~f(t), z~tl.

If we now apply the substitution 1 z {x+f(a) l to Ez we can ask if P(y,f(z),z) and P(x,x,t). 1- P(f(a), f(a),t) are still unifiable. This implies the ques­ tion: are the substitution o and 1 unifiable.

o 1 · m.g.u. (f(t),f(a)) = lt~al

o2 · {t~a, y~f(a)l

o 3 · the most general unifier · {t~a, y~f(a), z~a l and this is also the most general unifier of P(y,f(z),z) and P(x,x,t).T z P(f(a), f(a),t).

4. Application of Substitution Unification

to Theorem Proving

Readers unfamiliar with the notions used in resolution theorem proving can find the necessary definitions in [5 and 2].

The application of our approach is strongly cvn­ nected with on the one hat~d the way the resolution principle is used and on the other hand with the representation of clauses in the computer memory. If the clauses are represented in the usual way as lists, there is no profit in using the algorithms stated in §3. The improvement in efficiency comes in when we represent clauses by two pointers point ··· ing to the parent clauses and by a pointer to the substitution applied in this resolution step L 1]. For this latter representation, using the unifica­ tion algorithm for expressions requires a search through the tree of pointers to make the actual clause since we want to know whether the literals are unifiable with the literals in some other clause. The advantage of using the substitution unification algorithm here can be seen right away.

We first compute the so-called classification matrix for the input-clauses [4J. The literals in the input clauses are numbered, let us say, from I to m and the matrix consists of substitutions. The (l,k)th entry is 0 if the lth literal is not uni­ fiable with the k-th lite~al; the entry is the most general unifier of the 1-th and k-th literal other­ wise.

We can state the following corollary of theorem 4 and 5 from 3. (unification for a resolution step).

If Land K are unifiable l i t erals with m.g.u. o (L and K do not have any variables in common) then Le 1 and K82 are unifiable iff e 1, e 2 and o are uni­ fiable; the most general unifier of {e 1 , e2, o} is also a unifier of L8l and K8 2 · (In 81, 82 occur only variables occu~ng inLand K respectively and 8 1 , 82 do not have variables in common)

Implementing this we have to take care of the conditions stated in parentheses; we will see how in an example stated below.

In case of factoring the situation is a bit different because there the substitutions 81 and 82 have variables in common therefore we have to treat factoring separately. The following situation occurs. Two literals L and K are unifiable with m.g.u. o; K and L do not have any variables in com­ mon because they come from different clauses. Sub­ stitutions o1 and 02 are applied to K and L re-· spectively and then the c lauses containing Ko1 and Lll2 are resolved <·n literals different from Ko 1 and L02, involving unifier A. The question to be an­ &wered now is: are Ko 1 ~ and L0 2 ~ still unifiable given Land K are unifiable with m.g.u. o.

THEOREM I. K81A and L82A are um:fiable in the above case iff o, 81,82 and A are unifiable. Them.g.u. of {o,8 1 . 8 2 ,A} is a unifier of K8 1 A and L8 2 ~.

PROOF. If {o,8 1,82,A} unifiable then K8 1A and L82A are unifiable. (follows directly from theorem 4, 3). If {o , 8Jt 82,Al are not unifiable ihen because 8), 82 and ~ are unifiable, o is not unifiable with e1ther 81, e2 or ~ -

Case I : x ~ t 1 E o; x ~ t 2 E e1 ve 2 VA with x E L u K.

If x ( L then t1 E K, in L82A x is replaced by t2 so K and L8 2 ~ are not unfiable so KA1A and L82A not unifiable.

Case II: x ~ y E o ; y ~ f(x) E e 1 v 82 v A, x E L, y ( K

y ~ f (x) t 0 1 v 8 2 · y ~ f (x) E A; so y in K is re­ placed by f(x) and KA and L not unifiable; if x, y E L the same follows: y ~ f(x) E 8 2 v A etc. 0

All together we can see that we are not espe­ cially interested in most general unifiers but we are interested in what happens to all variables in the input clauses during the deduction and that is what we have to keep track of. (see example).

Another application strikes the eye when we look at the theorem proving problem in a problem solving way: we start with some topclause denoting the disjunction of its literals, the goal we have to reach is to resolve away all literals (subgoal~ (and- branches), each of which can be resolved in different ways (or - branches). What makes things complicated is that the subgoals are not indepen­ dent [3,4]. Firstly we can assume that all new variables introduced in different branches are dif­ ferent from each other so that the only link be­ tween subgoals is the variables they have in common. This means that we have only to keep track of sub­ stitution components that effect those variables.

We want to prove that the most general in­ stance of 8 1 , ·.. ,8n is the ultimate solution to problem L1 ··· Ln if 81, ... ,8n are solutions to L 1 , ··· ,L respectively. The fact that literal L (subgoalY is solvable with substitution e (vari­ ables of left sides of the components all occur in L) means that there exists a refutation of L say Co · L, CI·····Cm = 0 where Ci is the resolvent of C·-1 with a clause Di-l (not necessarily a input­ clause) furthermore Do has to contain a literal K opposite in sign to L with IKI and ILl unifiable.

From this refutation we can find a derivation of an expression E · Ko with lEI and L unifiable with unifier 8 : cj- D 0 , C2, ..· ,c~ · Ko.

THEOREM 2. If there exists a refutation of literal L (unrestricted resolution) involving substitution 8 on L, then there exists a deduction of a literal K which has sign opposi te to L and where I K I and I J.l are unifiable .

The proof proceeds by induction on the length of the refutation.

Example

Given a set V and a multiplication operator · which is associative and left and right solutions are in V then we want to prove the existence of the iden­ tity element. To translate this into predicate cal­ culus we use the predicate P(x,y,z) which can be interpreted as X * y a z .

Problem input clauses:

1. P(g(x,y) ,x,y) 'Vxlty3z: Z*x=y.
2. P(x,h(x,y),y) 'VxVy3z: x·z~y.

).,P(x,y,z),P(y,u,y) P(z,u,z) 'VxVyVzVu[x·y=zAy·u= =y.z·u=z J

4.,P(j(x),x,j(x)) 'negation of the theorem: 3yVx: x·y=x.

We number the literals in the problem I to 6. (clause 3 containing lit 3,4 and 5) We first compute the classification matr i x:

0 means not resolvable (identical to: opposite in sign and the absolute values are not unifiable) . o 13 means literal I and literal 3 are resolvable involving subs titution 013 where variables occur­ ring, in literal I are indexed by I and variables occurring in literal 3 by 3 so making the standard­ izing apart quite easily. The f0llowing substitu­ tions are involved in the matrix:

We work this example out using connection graphs [4). If we use connection graphs it is al­ most necessary to use the substitution unification algorithm because the arcs between the clauses (literals) are in fact unifiers and new arcs can be computed from old arcs using this algorithm. The initial graph is made from the classification matrix:

Note that oi4 · o24 because we are only interested in those substitutions concerning variables in lit 2 and lit 4,5 .

Acknowledgement

Much of the novel ideas in the paper developed from discussions with members of the Computational Logic Department of the University of Edinburgh during a stay of the author. In particular I am in­ debted to R. KOWALSKI who also gave very useful comments on a first draft.