A New Hyperparamodulation Strategy for the Equality Relation

1 · Introduction

Equality is an important relation and many theorems can be easily symbolized through it's use. Important research with respect to the equality relation has been carried out in several directions by many authors. Darlington [2] used a second-order equality substitution axiom, and Robinson and Wos [13,11] proposed demodulation and paramodulation to handle equality. Along this line, Wos, Overbeek and Henschen[14] proposed a refinement of paramodulation called HYPERPARAMODULATION and McCune[8] proposed Horn semantic paramodulation. Along another line, there is the E-resolution system by Morris[9] for the treatment of equality. Later, Digricoli [3] proposed the RUE-NRF rule of inference following the lines of research proposed by Morris in E-resolution and by Harrison and Rubin[4] in generalized resolution. The Connection Graph Procedure introduced by Kowalski [ 5] represents all possible resolution steps by links between the complementary unifiable literals. In [ 12], the ideas of the Connection Graph Proof Procedure are extended to handle paramodulation. On the other hand, Knuth and Bendix created a procedure for deriving consequences from equality units using a reduction.

We remind the reader of the following problems itself. The sets of equalities P and D need not be disjoint. Their choice, in practice, is heuristic but at present, for the theory, P needs to be all of the equalities inS. Condition 3), which will be called the into-term-containment restriction, will be of specific importance in plan formation to be discussed in Section 4.

· Supported in part by the National Science

Foundation under Grant Number MCS-8306637

Definition. Let C1 be a k-para/demod link of a clause C relative to PUD and Ao,A11····Ak as above. If, for O<i<=k1 Ai is a paramodulant of Ai-1 then let Ei be the unifier of the paramodulator and the into term in Ai-1 · Otherwise, i. e. Ai is a demodulant of Ai-11 let Ei be the empty Substitution. Then k-E = ( ··· CCE1*E2)*E3) ··· Ek) is called a k-linked unifier of C1 from C, where · is the composition operator.

Definition. A partial unifier of terms/literals t 1 and t 2 having the same function/predicate symbol is a substitution which unifies t1 and t2 from left to right, skipping over any pair of ununifiable arguments.

Definition. A function subatitution link of a clause of the form f(t1·····tn)<>f(s1····Sn) VA is a clause D v A*E 1 where A is a set of literals, E is a given substitution to be applied to f(t1, ··· ,tn) and f(s1 1 ··· ,sn), and D is a disjunction of inequalities formed by the pairs of arguments not unified in f(t1···· ,tn)*E and f(s1 1 ··· ,sn)*E.

Definition. A predicate Substitution link of a pair of clauses of the form P(t1····tn) vA and -P(s 1, ··· ,sn) v B1 where A and B are sets of literals1 is D v A*E v B*E 1 where E is a substitution to be applied to PCt11···tn) and P(s 11 ··· sn), and Dis a disjunction of inequalities formed by the pairs of arguments not unified in PCt1 , ··· ,tn)*E and PCs1 , ··· sn)*E.

The substitution used · in a predicate or a function substi tution link may be the empty substitution, a partial unifier or a full most general unifier. In the last case, of course 1 D will be empty. In fact, in the experiments discussed in Section 5 we always used partial unifiers 1 and our program obtained proofs for all the problems tried. The role of the Substitution link is to simplify a clause by stripping off the outer function/predicate symbol of one of its literals. The soundness of rules of inference which generate function/predicate Substitution links can be derived directly by the use of the function and predicate substitution axioms. In our equality-reasoning system, the above two rules of inference will replace the use of function and predicate substitution axioms. This, in effect, restricts the use of those axioms by not allowing the generation of clauses corresponding to arbitrary resolutions from substitution axioms. However, unlike previous attempts in this direction (e.g., [3,4,9].), we will propose a system in which the rules themsel ves will be used in a very restricted way, further cutting down on the number of clauses they are allowed to generate.

We now define a new inference rule called HL(Henschen-Lim)- resolution.

Definition. Let S be a set of clauses, P be a set of paramodulators and D be a set of demodulators. Let N be the transitivity clause {x<>y y<>z x=z} in the equality axioms 1 A1 be a positive unit clause in S1 and A2 v B be a clause in s, where A2 is a negative literal and B is the set of the remaining literals. Let the variables in these clauses all be separated. Suppose that the set of clauses {A1, A2 v B, N} satisfies one of the following conditions:

1. (forward) There exists a most general unifier(MGU) E1 of A1 and the literal x<>y and a MGU E2 of A2 and L1 1, where L1 1 is a k-pd link of {x=z}*E1 relative to P U D with a k-linked unifier k-E.
2. (backward) There exists a MGU E1 of A2 and the literal x=z and a MGU E2 of A1 and L2 1, where L2 1 is a k-pd link of {x<>y}*E1 relative to P U D with a k-linked unifier k-E.

Then the clause (y<>z v B)*(k-E)·E2·E1 is called an lß..-resolvent of the set. N is called the nucleus clauae, and A1 and A2 v B are the satellite clauaes.

The terms of an (in)equality in A1 1 A2, P or D are allowed to be flipped if necessary to match. In particular 1 paramodulation proceeds from either side of any equality in P. Further this definition can be extended in such a way that A1 is an arbi trary clause in S. We can also allow A2 to be positive and link to y<>z in N 1 or A1 to link to y<>z 1 etc. For the rest of this paper, however, we use the definition as given above.

Definition. Given a set S of clauses 1 a deductio~ from S is called an lß..-deduction if and only if each clause in the deduction is a clause in s, an HL-resolvent, a regular resolvent or a function or predicate substitution link of an HL-resolvent.

Definition. An HL-deduction of the empty clause from S is called an lß..-refutation of S.

Eiample 1

Consider the E-unsatisfiable set of clauses:

1. k<>g(a)

2. f(h(b) ,c)=a

3. d=h(b)

4. e=c

5. k=l

6. i=f(d,e)

7. l=g(i)

An HL-refutation looks like:

Example 2

Consider the theorem if f(y,z)=f(z,y) in the group theory. x*x=e then

1. f(e,x)=x
2. f(g(x),x)=e
3. f(f(x,y) ,z)=f(x,f(y,z))
4. f(a,b)<>f(b,a)
5. f(x,e)=x
6. f(x,g(x))=e
7. f(x,x)=e

An HL-refutation looks like;

Co111111ents:

• 1). We do not allow function/predicate substitution to be used during the formation of the HL-resolvent, but only to the end result . We believe this corresponds to human-like approaches to function/predicate stripping. In any case, i t severely limits the way in which these rules are allowed to generate new clauses. Similarly, transitivity is used only as an HL-nucleus and only when two terms have been chosen for linkage. Symmetry is built in, so we don·t need to include x<>y y:x. But note that flipping equalities is allowed only if it will make some !arger deduction sequence work. So we have very tight restrictions on the uses of equality axioms.
• 2). As illustrated in the above example, we plan to use HL-resolution with the set-of-support strategy, reasoning from the denial of the theorem. Simple paramodulation with set-of-support and without function reflexive axioms is · known to be incomplete as the following example shows:

2. c=d

with only clause supported. Because the linkage in HL-resolution is allowed from either A1 or A2, we can often get around this problem, and the reader can verify that there is a supported HL-resolvent

using a 1-pd link from clause 3 which generates the function substitution link c<>d. The idea is that we reason from a supported clause and another clause, and the direction of the linkage shouldn't matter.

1. Although the above is a cooked up counterexample, the Situation is totally different when demodulation is used. Then most normal problems are not refutable by paramodulation using only the denial as support. For example, the first backward reasoning paramodulation step in the x*x=e problem is to generate f(e,f(b,a))<>f(a,b), which immediately demodulates back to f(b,a)<>f(a,b). Since HL-resolution is a hyper rule, demodulation is blocked on all the intermediate steps. A corallary of this Observation is that if a k-pd link starts out with a number of equalities used backwards, somewhere in the linkage a non-demodulator equality must be used or else the target term must rearrange the built-up term. Otherwise the entire HL-resolvent will just redemodulate. We believe this feature also matches that of human-style equality reasoning in which people often purposely make complicating Substitutions into terms with the goal of being able to reassociate, distribute or some other such.
2. 4). As with other hyper methods, the idea is

to keep only the end resul t, which hopefully will be a more meaningful one. For equality we believe this may also lead to the possibility of some high level planning. For example, in the k<>g(a) problem above, there are several HL-resolvents starting from k<>g(a). However, only the given one leads to function stripping. Thus, one heuristic in choosing A1 and A2 for HL-resolution is to pick terms with the same outer function symbol when possible. Further in the given example, we can note that there is linkage between the arguments, a and i, of the two terms that were resolved, further indicating that k<>g(a) and l=g(i) might be a profitable choice. Such analysis will be facilitated by the use of the equality connection graph to be described below. We have only begun to consider these ideas, but believe they may lead to interesting results. We believe the idea of choosing two terms and attempting to link them through the graph makes HL-resolution perhaps more amenable to such heuristic analyses than other eq uali ty systems. In any case the generation of paramodulants is, again, controlled and directed by the choice of A1 and A2, which choice could be made by some high level planning process or even human

interaction.

• 5). Note that we could pose the rule strictly in terms of paramodulation without recourse to a nucleus and resolution at the last step. However our approach emphasizes the notion that we are looking for OUTER-LEVEL linkages, and especially those that lead to potentially useful function/predicate stripping. Furthermore, it provides target terms to be linked.

3. Co·pleteness

The basic idea is that, from the existance of an unrestricted paramodulation deduction, we construct an equivalent HL-deduction. Proofs of the

following Lemmasand Theoremsare found in [6].

Le.ma 1. If S is an E-unsatisfiable set of UNIT, EQUALITY clauses including x=x and functional reflexive axioms, then S has a refutation with a negative clause as top clause by paramodulation and resolution whose paramodulators are unit clauses in s

Lemma 1 shows that there always exists an unrestricted link between the negative clause and the last clause of the proof in the unit case. The only problem is the restriction of into term containment. We know that a paramodulation deduction tree can be rearranged into subsequences of deduction in such a way that all paramodulations in a subsequence are into one side of the inequality. For example, the deduction

can be rearranged so that the two paramodulations into the right side are done first. Note, it cannot be rearranged so that the paramodulation into the left side is done first unless a new step using g(y)=g(y) is used. Note, however, that each subsequence into the same side will correspond to

one or more HL-resolvents.

Le..a 2. A given clause t<>t' and a

which generates a paramodulant tn<>t", where

1. The paramodulation sequence in T can be arranged according to the order of argument positions in the outer term of ri, 1<=i<=n-1,
2. The terms t and t1 are unifiable,
3. t"=t'*E(T), where E(T) is the composition of unifiers in T, and
4. The last paramodulation only is paramodulation into the outer term itself whose from term is not a variable,

can be transformed into an HL-deduction which generates an HL-resolvent that is the same as tn<>t" within the alphabetic variance.

Theore. 1. If S is an E-unsatisfiable set of UNIT, EQUALITY clauses including x=x and functional reflexive axioms, then S has an HL-refutation with the choice that the sets of paramodulators contains all the positive equality clauses in s.

Theore· 2. If S is an E-unsatisfiable Horn set of EQUALITY clauses including x=x and the functional reflexive axioms FR, then S has an HL-refutation with choice of the set of paramodulators as above.

Corollary 1. If S is an E-unsatisfiable Hornset of clauses including x=x and the functional reflexive axioms FR, then S has an HL-refutation with the same choice of the set of paramodulators as above.

While completeness is important to know about, it is more important in our view to develop effective proof procedures. Thus, for example, we would not recommend using FR(Function Reflexive) axioms. We have seen in Section 2, Comment 2 that for some cases where FR is required in simple paramodulation, HL-resolution proofs exist without FR because we are allowed to link either forward or backward. Whether HL-resolution is complete without FR (perhaps with some other restrictions relaxed) remains open. However, in practice we do not

recommend using them.

Also we believe that in practice P and D

will not be chosen to be both all of S. Again, we do not have a theory as to how they may be restricted and still maintain completeness . Indeed we are only beginning to consider practical aspects of choosing P and D. This is an area for considerable further study and experimentation.

Finally, we note that the use of HL-resolution (or any paramodulation rule) with only the negative clause as support eliminates the generation of positive equalities. This may not be advantageaus in view of the effective use of new demodulators in [10]. Wehave not experimented with the generation of HL-resolvents in which A1 and A2 are both positive. This also is an area for considerable further investigation.

4. Plana for k-pd LiDking

Clearly a major part of HL-resolution is to determine if there is one or more k-pd links between the chosen target terms. The restrictions on and properties of k-pd links suggest the use of an equality graph to aid in finding links, very much like regular connection graphs are used in finding resolutions. The basic idea is to form a graph at the beginning of the run in which terms that could potentially paramodulate at the outer level are connected and the corresponding unifiers are formed. Then two candidate terms for HL-resolution can be attached to the graph. Paths of length less than the bound for k which connect both the outer terms and inner terms can then be easily found and the corresponding set of unifiers

tested for compatibility as in (1].

We now present some definitions leading up to such a graph mechanism and the formation of HL-resolution plans for a pair of terms.

Definition. Let P be a set of positive unit equality clauses. An equalitJ graph (EG) is a graph such that

1. To every left or right term of equality, there corresponds a node whose label is the term.
2. Two nodes are oonnected if their terms are unifiable after renaming variables so that different clauses contain different variables. The most general unifier is the label of the edge.
3. Nodes corresponding to terms which beleng to the same equality clause are grouped together in the graph. The clause number is the label of the group.

Since a group of nodes in an equality graph consists of only two nodes, the notation i+ (or i-) will be used to represent the right (or left) node in the group i, -i+ (or -i-) represents the node i­ (or i+) which is the other term in the group i, and

i* denotes i+ or i-.

Definition. A liaking path between two terms to and tn is a path in the equality graph of the form

to -- t1=s1 -- t2=s2 -- ··· -- tn-1=sn-1 -- tn where, ti =si is a clause and to links to t1 and each si links to ti+1· The length of this linking path is n.

Definition. Let the linking path between two terms s1 and tn+1 be

where the variables in all clauses have been separated and Ei, 1<=i<=n, is a MGU of Bi and ti+1· If E=E1*E2*···*En is defined, where · is the operation of oompatible composition, then the linking path is said to be link ~tible and E is called a link compatible unifier.

Definition. Let a term f( t 1 , t2, . ··· , tn) have a link compatible unifier Ei for each argument ti to a k-pd link ti', 1<=1<=n. If E=E1*E2*· ·· *En is defined, then the term f( t 1 , t2, ··· , tn) is said to be tera compatible and E is called a term

compatible unifier.

Definition. An augMnted equalitJ graph of a term t for a term s, denoted by AEG(t,s), is an equality graph as above with the two extra groups of nodes {t} and {s}, where,

1. All nodes in EG whose labels are unifiable with t or s are connected to t or s, respecti vely, with a labeled link labeling the unifier.
2. All nodes in EG whose labels have the same outer function symbol as t but are not unifiable with t are connected to t with an unlabeled link.

The labelad link is used for checking compatibility in finding a paramodulation sequence and the unlabeled link is for finding inner level target terms, which will be described below.

Definition. A plan Plan(t,s) of a term t for a term s is a set of tuples of the form (<I1*· I2*· ··· , Ik*>, k-E, r), where,

1. In the sequence <I1*· I2*· ··· , Ik*>, Ij, 1<=J<=k, is a group number and Ij* represents a left or right node (from term) depending on the sign of ·.
2. k-E is the composition of the labels (unifiers) of the linking path s -- I1 -- I2 -- ··· -- Ik from s to Ik·
3. r is the term formed by paramodulating the paramodulators in the sequence <I1*· I2*· ··· , Ik*> into the term s in their order.

Rather than trying to build k-pd links of a term t which are to be resolved with a term s in an ad hoc way, a systematic method like target-driven search can be devised using the restrictions on the k-pd link. Since a k-pd link has the restriction of into-term containment, any into term should not be properly contained in any proceeding into-term.

Suppose we try to find all k-pd links of a term t which are to be resolved with a term s. 1) case 1: t is a constant or variable.

In this case, the linking process is simple due to the into-term-containment restriction. In fact, all the position vectors of the into-terms in the seq uence are the same, 1. e. , the outer level position vector.

2) case 2: t is complex term

Let t be a complex term f(t,,t2,. ·· ,tn>· There will in general be many into term candidates at the beginning of the linking process. Furthermore, it seems difficult to know when to terminate an inner level linking sequence. We propese a method, which we call target-driven search, that works backwards from s rather than forwards from t. Step 1)

Try to find outer level links of s which are either unifiable with t or have the same function symbol as t and are of length no greater

than the bound on k.

Step 2)

Let s' be one of the outer level links of s.

Subcase 1): s' is unifiable with f( t 1 , t2, .·· , tn). Then, by the compatibility of unifiers on the k-pd link, there exists a k-pd link of t on the path t--s·-- ·.. --s. Therefore we have found a k-pd link.

Subcase 2): s' is not unifiable with t but has the same function symbol f. Let s 1 be of the form f(s1,s2·····sn). Now we can break down the linking process into sub-linking processes of finding k-pd links of t1 to s1, t2 to s2, ··· , and tn to sn· The sum of the lengths of these links and the length of the link from s to s 1 must be bounded, which narrows the search considerably. Assume that all sub-link paths wi th compa ti ble composi tions E 1 , E2, ... , En respectively are found. If E1, E2, and En are compatible, then f(s1'·s2', ·.. ,sn'), where si'· 1<=i<=n, are k-pd links of si, is checked to see if it is unifiable with t. If they are unifiable, there exists a k-pd link of t on the path f(t1,t2·····tn)--f(s1'·s2'·····sn')-­ --f(s1,s2·····sn)--··· --s.

Note that if s' is neither of those two cases, there is no link between t and s' because of the restriction of into-term containment.

5. r.pla.entation aod Expert.entation

We have implemented HL-resolution on NUTS (Northwestern University Theorem-proving System). NUTS is a programmable, interactive theorem proving system based on LMA (Logic Machine Architecture) [7]. The main part of the additions to NUTS centers on a pair of algorithms, based directly on the comments in Section 4, which generate first the set PLAN(t,s) of all plans for the two terms t and s and second the set PDLINK(t,s) of all k-pd links.

• A primary purpose is to compare HL-resolution and paramodulation, so we didn't try any open problems yet but included problems from group theory and ring theory.

In the experiments reported on below, we made several restrictions. In linking process, no paramodulation was allowed from or into variables, as is the standard in most paramodulation experiments. Since HL-resolution may generate an HL-resolvent using 0-pd link, in the case that one of from-term or to_term happens to be a variable, the HL-resolvent is, in fact, a paramodulant genetated by paramodulation from or into a variable. But that is not a severe problem because it is allowed only from or into outer level term. We placed a bound on k in such a way that we did't allow more than 1 paramodulation at a position. An interesting restriction is to not allow the same paramodulator to be used at tbe aa.e position more than once in the link. Of course, we did not use the functional reflexive axioms. As remarked above, it is an open question as to the effect of these restrictions on completeness. However, they are necessary for effectiveness in both HL and regular paramodulation.

In all experiments, we picked the clause with the fewest number of symbols for the next step. In the case of HL-resolution, we always worked backward. For the paramodulation runs, we picked some positive clause as set-of-support, usually a clause from the special hypotheses and all paramodulators were applied only from the left to the right side of equalities. The clause used in a particular experiment are indicated in the tables below.

An important comment is that in the HL experiments we did not make use of any heuristics or human intervention in choosing a target term to link to or in filtering the HL-resolvents for retention except in the ring problems. There we used a very simple heuristic if the outer function symbol of the HL-resol vent did not also occur as an outer function symbol in some input clause, the resolvent was not kept. This gave extra emphasis to the notion of working on outside terms. The importance of this comment is that the HL format provides first a pair of target terms and second an end result that is much more significant and much more like a human level inference than ordinary paramodulation. We intend that HL-resolution be used with heuristics for better selection of target terms and "interesting" results. It is possible that some problems would admit good heuristics for selecting the target terms; certainly there are more intelligent possibilities than to just take the one with fewest symbols or to take any target for which there is a link as was done in our simple experiments. We also feel that there could be better heuristics developed for deciding to keep a clause or not based on the fact that an HL-resolvent is a !arger, more human-like step. In fact, in this last regard, one might even consider using HL-resolution in an interactive mode since the number of clauses presented to the user would be significantly less than in ordinary resolution or paramodulation. A user might be able to digest an analyse the limited number of these clauses and help direct the program's effort.

Legend: In the following report of experiments, the experiment ··h·· and ··p·· mean HL-resolution experiment and set-of-support paramodulation experiment, respectively. Further, A, P, D, S, and N represent Axiom set, Paramodulator set, Demodulator set, Supported clause set and Non-supported clause set, respectively. Here the axiom set is the set of clauses which can be used as satellite clauses.

Experiments

gihj and gipj are similar to the experiments gihdj and gipdj, respectively, except that no demodulation is applied to inferred clauses. In the tables below, the number of paramodulants used in the k-pd links of an HL run is given in parentheses under the paramod column.

Results

Boolean Algebra Experiments

bihj and bipj are similar to the experiments bihdj and bipdj, respecti vely, except that no demodulation is applied to inferred clauses.

Results

Ring Theory Experiments

Experiments

rihj and ripj are similar to the experiments rihdj and ripdj, respectively, except that no demodulation is applied to inferred clauses.

Results

6. Conclusion

We proposed a new inference rule called HL-resolution for the equality relation that is intended to have the benefits of hyper steps and to control the uses of paramodulation. It generates a resolvent by building a paramodulation/demodulation link between two terms using a preprocessed plan as a guide. We proved completeness for Horn sets and suggested an efficient method for implementation. A number of experiments were conducted on problems in abstract algebra and the resul ts are encouraging. But many problems remain untouched. Completeness without Function Reflexive axioms possibly with some other restrictions relaxed remains open. And we do not have a theory as to how to restriet the choice of the sets of paramodulators and demodulators and still maintain completeness or effectiveness. We have not, as yet, considered what strategies for choosing pairs of target terms might be effective nor experimented with different target strategies. Equally important is the question of whether or not a program might be able to select only the profitable links from the set PDLINK(t,s). In our experiments, we simply generated all HL-resolvents possible within the bound on k. As mentioned earlier, we believe HL-resolvent has more potential for developing effective heuristics because of the format - there could be heuristics for picking target terms, and heuristics for selecting k-pd links. Further, an HL step is a larger, potentially more significant step; we feel that it could be easier to predict the utility of such a larger step than to do the same for a series of shorter steps. Whether or not this potential can be really developed remains to be seen.

7 . Heferences

1. Chang, C. L. and R. C. T. Lee, Symbolic ~ And Mechanical Theorem Proying, Academic Press, 1973.
2. Darlington, J. L., "Automated Theorem Proving with Equality Substitutions and Mathematical Induction," in Machine Intelligence, Vol. 3 (B. Meltzer and D. Michie, eds.), American Elsevier, New York, pp.113-127.
3. Digricoli, V. J., "Resolution by Unification and Equality," Proceedings of 4th Workshop on Automated Deduction, 1979, Texas.
4. Harrison, M. and N. Rubin, "Another Generalization of Resolution," J. ACM, Vol.25, No.3, July 1978, pp341-351.
5. Kowalski, R. , "A Proof Procedure Using Connection Graph," JACM 22,4, 1975.
6. Lim, Younghwan, "A New Hyperparamodulation Strategy for the Equality Clauses", Ph.D Dissertation, Northwestern University, 1985.
7. Lusk, E., W. MaCune and R. Overbeek, "Logic Machine Archi tecture: Kernel Functions," Proceedings of the 6th Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 138, 1982 .
8. McCune, W., Semantic Paramodulation for Horn Sets, Ph.D. Dissertation at Northwestern University, 1984.
9. Morris, J., "E-resolution: an Extension of Resolution to Include the Equality Relation," IJCAI, 1969.
10. Overbeek, R., J. MoCharen and L. Wos, "Complexity and Related Enhancements for Automated Theorem-proving Program," Comp. and Maths. with Appls. Vol.2, No.1-A, 1976, pp.1-16.
11. Robinson, G. A. and L. Wos, "Paramodulation and Theorem Proving in First Order Theories with Equality," in Machine Intelligence Vol.4 (B. Meltzer and D. Michie, eds), American Elsevier, New York, 1969, pp.135-150.
12. Siekmann, J., and G. Wrightson, "Paramodulated Connectiongraphs," Acta Informatica, 1980.
13. Wos, L., G. A. Robinson, D. F. Carson and L. Shalla, "The Concept of Demodulation in Theorem Proving," JACM, Vol.14, No.4, October 1967, pp.698- 709.
14. Wos, L, R. Overbeek and L. Henschen, "HYPERPARAMODULATION: A Refinement of Paramodulation," Proceedings of the 5th Conference on Automated Deduction, 1980.