E-Resolution: Extension of Resolution to Include the Equality Relation

I. Introduction

E-Resolution is a technique for automatically generating proofs of theorems in the first-order predicate calculus with equality. The mechanism by which substitution of equals for equals is handled is automatically part of E-Resolution, or "built-in." The completeness of E-Resolution has not, as yet, been proven, and it is therefore not known whether or not the system is complete. However, the author is currently investigating this topic.

E-Resolution incorporates and combines some ideas similar to those used in Paramodulation, 8 k-modulation,lO and Sibert's thesis,9 but is dif­ ferent from all three. Some of the features which

enhance its usefulness are:

• (a) It is not necessary to add special axioms for equality to the original set of clauses, i.e., axioms for symmetry, reflexivity, transitivity, and substitutivity.
• (b) The mechanism of equality substitution is not activated until its success could help produce a resolvent. This causes the number of inter­ mediate clauses which must be retained in the proof of a theorem to be held to a minimum.
• (c) The system is a direct extension of J. A. Robinson's Resolution principle4 and is de­ signed so that (hopefully) search techniques developed for Resolution can be used, without extensive modification, in E-Resolution. At least this seems t9 be the case for set of support strategy, 11 maximal clash resolution, 5 · 7 and merging.l

*This investigation was supported in part by Public Health Service Research grant GM-15769 (NIH).

James B. Morris* Department of Computer Sciences The University of Texas at Austin

The system is programmed in LISP and is running on the CDC 6600 as the main ~ortion of a theorem proofchecker for Set Theory. It has been used to prove several modest theorems involving equality

substitution.

The following sections serve to formally de­ scribe E-Resolution. Section II introduces defi­ nitions which will be used later. Section III develops the E-Resolution system, and Section IV illustrates E-Resolution through examples. Fi­ nally, Section V discusses search strategies.

II. Definitions

The following definitions are preparatory to the matter of defining E-Resolution. It is as­ sumed that the reader is familiar with the nota­ tion used in [4] and [6]. Such terms as atom, literal, clause, well-formed expression, substitu­ tion, disagreement set, Herbrand universe, etc. are defined there.

It is well known that any set of sentences in the first-order predicate calculus with equality can be converted to clausal form, i.e., an equiva­ lent set of clauses, each of which is a disjunct of literals. In the following definitions, we borrow heavily from [8].

Equality atoms. An equality atom is an atom whose predicate symbol is the special symbol"=". Rather than writing an equality atom as "=2ab", we will use the more readable "a = b". Note that the predicate symbol "=" is always of degree 2. Analo­ gous to the above, "12ab" is known as an inequality atom and will be written as "a I b". We will some­ times speak of equality literals and inequality literals. An equality literal is an equality atom or a negated inequality atom. An inequality lit­ eral is an inequality atom or a negated equality atom.

Interpretation. An interpretation I of a set S of clauses is a set of literals such that for each atomic formula F that can be formed from a predicate symbol of degree n occurring in S and n terms from the Herbrand universe Hs of S, ex­ actly one of the literals F or NF is in I. An interpretation I is said to satisfy a ground clause C if at least one literal inC is also in I, and to falsify a ground clause C if the complement of every literal in C is in I. An interpretation I is said to satisfy a non-ground clause C if it satisfies every ground instance of C over Hs, and is said to falsify a non-ground clause C if it falsifies at least one ground instance of C over Hs· An interpretation I is said to satisfy a set S of clauses if it satisfies every clause in S, and is said to falsify a set of clauses if it fal­ sifies at least one clause inS. [] represents the empty clause, and is not satisfied by any interpretation.

E-interpretations. An E-interpretation of a set S of clauses is an interpretation I of S having the following properties: Let a , ~. and y be any terms in the Herbrand universe Hs of S and let L be any literal in I. Then

1. (a = a ) € I, and
2. If L 1 is the result of replacing some one occurrence of a in L by ~ and (a=~) € I, then L' € I.

Note that if I is an E-interpretation, then we can prove the following:

1. If (a=~) € I then (~=a) € I, and
2. If (a=~) € I and (~=y) € I, then (a=y) € I.

General E-propositions. A general E-proposi­ tion states that a set of clauses follows from some other set of clauses in the sense of the first­ order predicate calculus with equality. The gener& E-proposition which states that the set of clauses (Y 1 ,Y 2 , ... ,Ym} follows from the set of clauses (x 1 ,x 2 , .·· ,Xn} is written as

and is taken to mean that if an E-interpretation I satisfies (x 1 ,x 2 , ... ,Xn} then it also satisfies (Y 1 , Y 2 , ... , Ym}. We sometimes write S->JJ to mean that S is an E-unsatisfiable set of clauses, i.e., there is no E-interpretation which satisfies S. If there is an E-interpretation which satisfies some

set of clauses S, then S is said to be E-satisfiab~.

III. E-Resolution

E-Resolution is a single-inference principle from which proofs of theorems in the first-order predicate calculus, with equality, may be obtained. Given a set S of E-unsatisfiable clauses which is in clausal form, E-Resolution attempts to find a proof by the application of the following simple process:

1. Initialize tree level bound k to zero.
2. Is 0 in S? If so, a proof has been found. Otherwise, add one to k and go to step 3.
3. Generate all E-Resolvents of S at tree level bound k, and add them to S. Go back to step 2.

There are two types of E-Resolvents. As an example of the first type, suppose that C and D are the two clauses

and there exist clauses B 1 , .·· ,Bi, which are inS, where A,B,E 1 , .·. ,Ei are disjunctions, and none of the C,D,B 1 , ··· ,B 1 have any variables in common. If 9 is a subst~tution such that

then

is an E-Resolvent of C,D,B 1 , ·.. ,Bi' in which case, the literals

are said to be resolved upon; in general, there are more than two literals (with the same predi­ cate symbols) in clauses C and D which are re­ solved upon.

As an example of the second type of E-Resol­ vent, suppose that C is the clause

and that there exist clauses B 1 , ··· ,Bi, which are

inS, where A,E 1 , ..· ,Ei are disjunctions, and none of the C,B 1 , ·.. ,Bi have any variables in common. If 9 is a substitution such that

then

is an E-Resolvent of C,B 1 , ··. ,Bi' in which case the inequality literal

is said to be resolved upon; in general, there are more than one inequality literals in clause C which are resolved upon.

This may be compared to Resolution 4 in which the terms in the argument lists of sets of literals L~ C and M~ D must be unified in order for the resolvent using L and M to exist. Equi-unification, however, upon finding that two terms cannot be uni­ fied ponders the question: Are the terms equal? Using a device known as the equality tree genera­ tor, all possible ways of satisfying equality of the two terms using equality literals from the current E-Resolution clause set En(S) (nth E-Resolu­ tion), is discovered. This discovery process may or may not introduce new literals as part of the

E-Resolvent.

The above process is described and formalized in the definitions appearing below. Readers fa­ miliar with [4] will note a similarity between many of the definitions there and certain defini­ tions below. This is done purposely, so that those r eaders will be able to understand E-Resolu­ tion more easily.

The equality tree generator (ETG). The equal­ ity tree generator is a formal device for specify­ ing all possible ways in which a term a may be trans formed into a term ~ by means of equality substitutions in some finite universe of equality relationships. The equality relationships are de­ fined by equality literals in some set of clauses, CEQ· Another input to ETG is an integer k, known as the tree level bound, which specifies a maximum node level bound on the equality tree. The reader is urged to refer to the example (Figure 1) as an aid to understanding the definition.

Every node in the equality tree T, generated by ETG, has a name which is an ordered triplet (y,c,e) where y is a term, C is a clause, and e is a substitution. The root node of T is named (a[J,€). A son node ofT is formed from node {y,c,e) as follows:

If there is a most general unifier a of y and ~. then the only son node of {y,c,e) is (~a,ca,ea). Otherwise, let D be a clause in CEQ which has no variables in common with any other clause. Let L be an equality literal o = w, or w = 5 , appearing in D. Select a term s which occurs in y and such that s and o are most generally unifiable with most gen­ eral unifier a. Let y 1 be the result of sub­ stitution of ma for a single occurrence of sa in ya . (Compare this with Paramodulation in [8].) Then the son node of {y,C,e) associated

with D,L, and s is

{y 1 ,(D-(L})a u Ca,ea).

A son node N 1 formed from node N = {y,c,e) by the above-described process is said to have been gen­ er ated from N. The clause D which is used to gen­ erate N 1 is said to be the clause associated with N 1 · If no clause was used from CEQ in generating N 1 , then there is no clause associated with N 1 ·

Two nodes {y 1 ,C 1 ,9 1 ) and {y",C",S") are called equivalent if y 1 is identical to y" and C 1 is a variant of C". The tree T is said to be fully­ formed at node N = (y,c,e) if no two son nodes of N are equivalent and there is no way to generate a new son node from N which is not equivalent to some existing son node of N. A node N is said to be terminal if (1) N has no son nodes and T is fully-formed at N, or (2) N = {y,C,e) where ( y,D, A) is an ancestor node of N, for any D and any A. Otherwise, it is said to be non-terminal. An equality tree T is fully-formed if it is fully formed at every node in T which is not a tip node and every complete branch beginning at the root

either

• (a) contains k+l nodes, where k is the tree level bound, or
• (b) ends in a terminal node (y,C,e), and there does not exist a A such that ~A is iden­ tical to y, or
• (c) ends in a node (possibly non-termjnal) (~A ,C,e), for some A. Nodes of this type are termed equality solution nodes. The set of clauses which are associated with all the nodes on the branch of T down to and including ( ~A ,C,e) is called the clause set associated with the e solution node (~A,C,e .

The equality tree generator produces a full-formed equality tree, given terms a and ~ . tree level bound k and set of clauses CEq·

As an example of the operation of ETG, sup­ pose a = f(a), ~ = g(h(c)), and CEQ is the s.et of clauses ( (f(x) = g(x) ,Qx), (a = c, Pz), (w = h(w)) ). Then a portion of the equality tree resulting from the a,~ and CEQ given appears as Figure 1. The nodes marked T are terminal; those marked P are not yet fully-formed; those marked E are equality solution nodes, and those unmarked are fully­ formed nodes.

Equi-unification algorithm. The equi-unifica­ tion algorithm is the key to E-Resolution. It is applicable to any finite, nonempty set A of well­ formed expressions, set of clauses CEQ containing equality literals, and tree level bound k.

Briefly, an explanation of the operation of the algorithm is as follows: (For this explana­ tion, we shall assume that the set A consists of two literals, Ps 1 s 2 ... sn and Pt 1 t 2 ... tn.) Start withE= 0. For each (s.,ti) pair, the algorithm attempts to find a most ~eneral unifier A which will make siaA = tiaA, where a is a substitution resulting from the unifiable (s . ,t.) pairs, for all j < i. If this is not posslbl~, however, it adds the inequality sia # tia ~here si and ti are distinct, corresponding terms occurring ins. and t . ) to the set E and makes a substitution ofLt. a L L for sia in A, only for that occurrence of sicr in Ps 1 s 2 ... sncr. When the above process is completed for all pairs (si,ti), the set E is examined. If E = 0, then A is most generally unifiable in the sense of [4]. However, if E # 0, then the set EcrA is processed as described below. Note the use of EcrA rather than E, where crA is the substitution obtained from the pairs (si,ti) which were unifiab~

Now, for each a # ~ in EcrA, ETG is activated with a , ~,Ek-l(S) and k as inputs. If for some a # ~ in EcrA, ETG cannot find a way to show that a = ~ . at tree level bound k, then the algorithm fails to find an equi-unifier at tree level bound k and terminates; otherwise, A is equi-unifiable.

The equi-unification algorithm is defined to be

• Step 1. Set cr 0 = €, i to Step 2. 0, E 0, P = 0, and go
• Step 2. If Acr i is not a singleton, go to Step 3. Otherwise, set E = Ecri and go to Step 4.
• Step 3. Let Vi be the earliest, and Ui the next earliest, in the lexical ordering of the disagreement set Bi of Acri. If Vi is a variable, and does not occur in Ui' set cr .+l = cr .(U./V.), add 1 to i and return to 1 1 1 1 Step 2. Otherwise, set E = E U (V /' Ui), substitute Ui in Acr i for just that single occurrence of Vi in the disagreement set Bi and return to Step 2.
• Step 4. If E = 0, then set crA = cri and terminate (equi-unifiable). Otherwise, set L equal to one of the inequalities, V. ~ U., in J J E, set E = E- (L), and activate the equality tree generator with Vj and Uj as the a and ~ arguments, k as tree level bound, and the set Ek-l(s) (see below) as the argument CEQ' where Ek-l(S) is the current E-Resolution set. Go to Step 5.
• Step 5. If the fully-formed equality tree T pro­ duced by ETG has no equality solution nodes, then terminate (failure to equi­ unify). Otherwise, select a node (y,~,e) from the finite set of all equality solu­ tion nodes in T, set P = P U ((y,~,9)},

set E = E9 and return to Step 4.

Partial equi-unifiers. If A is a finite, non-empty set of well-formed expressions for which the equi-unification algorithm terminates in Step 4, the substitution aA available as output is called the partial equi-unifier of A, and A is said to be equi-unifiable. The set P availabl e as output from the equi-unification algorithm is termed the equality solution node set. The union of all the clause sets which are associated with each of the nodes in the equality solution node set is called the equality solution clause set associated with P.

Key quintuples. The ordered quintuple (L,M,N,B,E) is said to be a key quintuple of the ordered pair of clauses (C,D) if the following conditions are satisfied:

1. L and M are non-empty sets of literals (which do not involve either the "=" or "~ predi­ cate symbols), and L <;;;; C, M <;;;; D where C and D have no variables in common with any other clause.
2. N is the set of atomic formulas which are members, or complements of members, of the set L U M.
3. N is equi-unifiable, with partial equi­ unifier aN, P = ((y 1 ,B 1 ,e 1 ), (y 2 ,B 2 ,e 2 ), ... , (y ,B ,9 )) is an equality solution node set n n n available as output from the equi-unification algorithm, B = B 1 U B 2 U .·· U Bn' and

E = (E 1 ,E 2 , ..· ,Em} is the equality solution clause set associated with P.

1. I f e is the substit tion e 1 e 2 ..· en' where the e i are those mentioned in (3) above, then either NoNe is a singleton, or corresponding distinct terms occurring in the argument lis ts of all the literals in NoNe are term components of the node names which are at the root node and equality solution node ( yi,B_t,9J of some branch of some equality tree. Also, every member of LoNe has the same logi­ cal sign, every member of MoNe has the same logical sign and no two members of LoNe and MoNe, respectively, have the same logical s~ The substitution oE= oNe is termed the equi­ unifier of the set N.

Key quadruples. The ordered quadruple (M,N,B,E) is said to be a key quadruple of the clause C if the following conditions are satisfied:

1. M is a set consisting entirely of inequality literals occurring inC, where C has no vari­ ables in common with any other clause.
2. If M is (ex 1 1 t3 1 , .·· ,ex/ f3i}, then N is the set (l(exl, ·· · ,exi),l(t3l'"···t3i)}.
3. N is equi-unifiable, with partial equi-unif~ 0N' p = ((yl,Bl,el)' (y2,B2,e2), ..· ,(yn,Bn,ed} is an equality solution node set available as output from the equi-unification algorithm, B = Bl U B 2 U ··. U Bn' and E = (E 1 ,E 2 , ·.. ~m} is the equality solution clause set associated
4. with P.
5. If e is the substitution e 1 e 2 .·. en' where the ei are those mentioned in (3) above, then either NoNe is a singleton, or distinct cor­ responding terms occurring in the argument lists of the literals in NoNe are term components of the node names which are at the root node and equality solution node (y.,B . ,e.) of some branch of some equality ]. ]. ]. tree. The substitution oE = oNe is termed the equi-unifier of the set N.

E-resolvents. An E-resolvent of the clauses

C,D,E 1 ,E 2 , ··· ,Em is any clause of the form

where (L,M,N,B,E) is a key quintuple of (C,D), or an E-resolvent of the clauses C,E 1 ,E 2 , ··. ,Em is any clause of the form

where (M,N,B,E) is a key quadruple of C.

E-r.esolvent at tree level bound k. An E­ resolvent at tree level bound k is any E-resolvent produced by restricting the equi-unifica tion algo­

rithm to tree level bound k.

Ek-resolvent sets. The Ek-resolvent set of clauses C,D,E 1 ,E 2 , ··. ,Em (or C,E 1 ,E 2 , ... ,Em) is just the set of all possible, distinct E-r~solvents at tree level bound k of C,D,E 1 ,E 2 , ·.. ,Em (or C,E 1 , E 2 , ··. ,Em). Note that for any sets of literals L c C and Me D, it is possible to generate more th~n one E-r;solvent at tree level bound k, since we may call the equi-unification algorithm more than one time for each set of literals L and M, each time selecting different equality solution nodes, as specified in Step 5 of the algorithm, to obtain different equality solution node sets. However, there are only finitely many ways to se­ lect the nodes and eventually a point will be reached where, for a given L and M, we cannot generate any new, unique E-resolvents at tree level bound k. In a practical system, it is fairly sim­ ple to organize the program in such a way that the equi-unification algorithm is actually called only once for a given L and M, while still obtaining all of the possible E-resolvents at tree level

bound k.

Ek-resolution. If S is any set of clauses, then the Ek-resolution of S denoted by Ek(S), is the union of S with the union of all Ek-resolvent

sets of members of S.

Nth E-resolution. The nth E-resolution of S, where S is , any set of clauses, is denoted by En(S), n ~ 0, and is defined to be S, if n = 0, and En(En-l(S)) otherwise.

IV. Examples

The first two examples are trivial examples which illustrate interesting points about the system,and the third example is a theorem from Set Theory. 3

Example 1. Given the clauses

1. (ex
2. f3, Qx}
3. (13 y}
4. (ex y, Px}
5. (Rex}
6. (~Ry}
7. (~Qx}

From (4), (5), (1), and (2) and the key quintuple

where the equality-tree generated is:

we obtain

Note that it is also possible to conclude (by choosing a different key quintuple)

From (6) and (7) it is obvious that we conclude

The above example illustrates what happens if there is more than one way of proving two terms equal. Note that if E-resolution had been designed so that it assumed only one way of proving a and ~ in the above set equal, the resolvent selected might possibly by (7'), in which case 0 cannot be con­ cluded. Unless the path a = ~ = y is recognized, it is impossible to deduce 0.

Example 2. (This example appears in a foot­ note in [8]. Suppose we are given the clauses

1. (a = b, Qc}
2. (g(a) -! g(b), ·Qc}
3. (c = d, ~Qc}
4. (g(c) -! g(d), ~Qc}.

This set of clauses is E-unsatisfiable and illus­ trates the necessity of those E-resolvents which are designed to remove inequality literals from clauses. Note that if we apply only those E-resol­ vents which are associated with key quintuples, we cannot deduce 0 from this set of clauses. We must also utilize those E-resolvents which are associated with key quadruples. From (1) and (2) with key quadruple

and the equality tree

we obtain

Similarly, from (3) and (4) with key quadruple

we obtain

From (5) and (6) we obtain

Example 3 . 2.40.3 in [3] . The following example is Theorem The theorem is stated as:

Previously proved theorems in [3] tell us

• (a) Theorem 2.24.6 (x n u = x)
• (b) Theorem 2.24.8 (0 n x 0)
• (c) Theorem 2.24.50 (x € y -+ (x € y) = U)
• (d) Theorem 2.24.51 (~(x € y) -+ (x € y) = 0)
• (e) Theorem 2.12 (x € y-+ X € U)
• (f) Theorem 2.34.5 (x € U -+ sng X € U)

where "sng" is the set operator which converts its one argument into a singleton set, e.g., sng a (a}.

The clauses numbered 1-6 below come from Theorems (a)-(f) above. Clause 7 comes from the negation of the theorem, and clauses 8-12 denote the clauses obtained in the proof of the theorem. For convenience, we denote "x n y" by f(x,y), "x € y" by the predicate Q(x,y) or the term g(x,y) "sng x" by h(x) and write the equality predicates in the more familiar manner. Also, U is the con­ stant denoting the universe, and 0 is the constant denoting the empty set.

1. (f(x,U) = x}
2. (f(O,x) = O}
3. (Q(x,y), g(x,y) = 0}
4. (~Q(x,y), g(x,y) = U}
5. (~Q(x,y), Q(x,U)}
6. (~Q(x,U), Q(h(x),U)}
7. (f(g(a,b), g(h(a),U)) -! g(a,b)}
8. (g(x,y) 0, Q(x,U)} from (3) and (5)
9. (g(x,y) 0, Q(h(x),U)} from (6) and (8)
10. (g(x,y) 0, g(h(x), U) = U} from (4) md (9

1. (g(a,y) 0} from (7), (1), and (10)

VI. Search Strategies

As stated earlier, it appears that set of support strategy, maximal clash resolution, and merging, as well as other search strategies suit­ able for Resolution may all be used without ex­ tensive modification in obtaining E-Resolution proofs. For example, maximal clash resolution is used in the theorem proof-checker discussed in (2].

The reasoning behind the statements in the above paragraph is simple. Note that E-Resolution proceeds exactly as does Resolution until (in Reso­ lution) two terms cannot be unified. At this poin~ E-Resolution makes a divergence. It checks to see if indeed these two terms which could not be uni­ fied, can be equi-unified. If this is the case, then a (possibly empty) set of literals, which are the by-product of equi-unification, will be unioned with the result of resolving (in the straight Re­ solution sense) the two clauses currently under inves tigation. Regardless of whether the two terms are equi-unifiable or not, E-Resolution be­ gins again at exactly the same point where the di­ vergence was initiated and proceeds from this point exactly as would Resolution, dependent upon whether the terms were unifiable or not. The only real difference is the set of by-product literals, which accumulate as a result of equi-unification, in E-Resolution.

Although no proof is given of the assertion, it seems true that for many of the same reasons that the above-mentioned strategies do not de­ stroy completeness in Resolution, they do not destroy comple.teness in E-Resolution.

Surranary

E-Resolution may be compared to other methods for handling equality substitutions in ~esolution, namely, Demodulation,lO Paramodulation, and the system described by Sibert.- 9

The Demodulation system is the forerunner of the more general, more powerful Paramodulation system. In the generating of equality trees by ETG , a portion of the technique used is very . similar to Paramodulation and Demodulation and Ln fact was inspired by the basic techniques of these two systems. However, in E-Resolution the only equality substitutions which result in a new clause are those which will produce an E-resolvent, al­ though many intermediate substitutions may be made in order to find the E-resolvent. In Paramodula­ tion, by contrast, equality substitutions may re­ sult in new cl auses which will not produce resol­ vents. This is the concept in E-Resolution which results in generation of only a minimum number of new clauses.

The Sibert system is more similar to E-Resolu­ tion than are Paramodulation and Demodulation.

However, it is felt by the author that E-Resolu­ tion is a more efficient system and, as such, in its present form is more practical for use on a machine. However, many of the concepts intro­ duced by Sibert are basic to the problem of Reso­ lution with equality and were used as a foundation for E-Resolution.

A disadvantage of E-Resolution and an area in which further research would no doubt increase greatly the efficiency of a system utilizing it, is the time which must be spent by ETG fruitlessly constructing an equality tree when, in fact, the a and ~ terms given it are not equal. In general, this condition will actually occur more times than will the condition where they are equal. However, the following process will rectify this problem: the tree level bound k may be set to some low level initially. A bound may also be set on the number of E-resolvent sets which may be generated, i.e., a maximum n such that En+1 (s) is not genera­ ted. Now, in generating En(S), one saves all equality trees associated with non-equi-unifiable literals of level k. If 0 is not in En(S), then one increases k to k' and restarts the E-Resolution process, each time extending and saving the equal­ ity trees associated with non-equi-unifiable literals at level k'. If 0 is not ill En(S), raise the ~ximum E-resolution level ~ to n' and generate En (S). If 0 is not in En (S), then k' is increased to k", etc.

Acknowledgements. The author would like to express appreciation to Dr. W. W. Bledsoe for much guidance, encouragement, and consultat ion given to him throughout the preparation of the E-Resolution system and the material presented here. The author would also like to acknowledge the valuable consultation given to him during his research efforts by Messrs. Robert Anderson and Forest Baskett.