The Efficacy of RUE Resolution Experimental Results and Heuristic Theory

1. Introduction

A primary reason for the failure of binary resolution relates to the handling of equality, a predicate which plays a central role in most axiomatic systems. The use of the equality axioms in the input clause set leads to very long proofs which are unnecessarily cumbersome and para­ modulation which leads to much shorter proofs presents problems of heuristic search for the proper paramodulants which experimentors have not

been able to surmount.

In [8,9) the author presented the theory of resolution by unification and equality in which the axioms of equality are· incorporated into the definition of resolution. In contrast to paramodulation, RUE resolution does lend itself to heuristics which converge to refutations and it is the purpose of this paper to carefully study this

issue.

We will first give a synopsis of the basic theorems and definitions of RUE resolution as presented in [9] and then proceed to the discussion of experiments and heuristic search procedures.

• (1.1) A disagreement set ~ ~ pair of terms (tl,t 2 ) is defined in the following manner:
• If t 1 ,t 2 are identical the empty set is the sole disagreement set.
• If t 1 ,t 2 are not identical, the set of one element the pair (t 1 ,t 2 ) is the origin disagreement set.
• If t 1 , t 2 have the form

THE EFFICACY OF RUE RESOLUTION

EXPERIMENTAL RESULTS AND HEURISTIC THEORY

Vincent J. Digricoli

Courant Institute of Mathematical Sciences New York University and Hofstra University 166-11 17th Road, Whitestone, New York 11357

then the set of pairs of corresponding arguments which are not identical is the disagreement set at the topmost argument level or more simply the topmost disagreement of t 1 ,t 2 ·

1. If Dis a disagreement set of t 1,t2· then D' obtained by replacing any member of D by the elements of one of its disagreement sets is also a disagreement set of t 1 ,t2'

In the simple example:

besides the origin disagreement, there are the disagreement sets:

The purpose of this definition is to define all possible ways of proving t 1 · t 2 , i.e. we can prove t 1 · t 2 by proving equality in every pair of any one disagreement set. An input clause set, for example, may imply equality in o 1 but not in o2 or o 3 · Or it may most directly prove t1 t2 by

proving equality in o 3 ·

In the sequence of derivable disagreement sets from topmost to bottommost, there is upward implication of equality, Oi+l + Oi· but not downward implication, Oi t Oi+l'

• (1.2) We proceed to define a disagreement set of complementary literals:

as the union of disagreement sets:

and We see immediately that:

where 0 now represents the disjunction of inequalities specified by a disagreement set of P,P, and furthermore, that:

where 0 is the disjunction of inequalities specified by a disagreement set of

We may now define our two rules of inference:

(1.3) The RUE Rule of Inference

"Given the clauses

and a substitution o, the RUE resolvent of a applied to these clauses is

where 0 is the disjunction of inequalities specified by a disagreement set of the complementary literals oP, oP."

(1.4) The NRF Rule of Inference (the-negative-reflexive function rule)

"Given A v t 1 ~ t 2 and a substitution a, the NRF resolvent of a applied to this clause is aA v 0, where 0 is the disjunc­ tion of inequalities specified by a disagree­ ment set of ot 1 , at2 ...

We have for example:

wh1c~ are obviously not equivalent we instead use the equality axioms resolution, each of the above one becomes an elongated sequence respectively. deductionR. If with unification step deductions of 3 and 6 steps

The two important issues which remain are the selection of substitution and disagreement set when we resolve complementary literals, for which there is the theorem:

(1.5) Completeness Theorem (Strong Form):

"A set of clauses is E-unsatisfiable if and only if there is an RUE-NRF deduction of the empty clause from S, in which we:

1. choose as a, the RUE-NRF unifier,
2. choose as 0, the topmost viable disagreement set,
3. satisfy the equality restriction when resolving complementary equality literals."

The reader will find in [9] a detailed treatment of the notion of viability which subtends the definitions of the above unifying substitution and also the equality restriction. It suffices to say . here that we- are to use the MGPU (the most general partial unifier) of P, P and this is a qualified form of the MGU of standard resolution, relaxed to permit irreducible disagrements.

The viability criterion enables us to suppress deductions which are recognized as provably irrelevant to a refutation and the equality restriction enables us to avoid useless variants of the same deduction path.

The above is a very cursory description of a quite substantial body of theory presented in [9].

2. An RUE Refutation in Group Theory:

Below we present an RUE refutation which proves that a group is commutative if x*x · e. The axioms of group theory are given in (4.3) of this paper. The style of proof is similar to that introduced by Harrison and Rubin in generalized resolution [7].

In formulating _ substitutions we are scanning complementary literals from left to right, skipping over irreducible disagreements, and furthermore substituting first at the topmost argument level and then at lower levels. This is evident in the first two steps of the refutation.

We are also being appropriately selective in choosing a disagreement set, sometimes using the topmost and sometimes the bottommost according to a criterion we will develop later in (5.2).

This 9 step proof becomes a 22 step proof when we use the equality axioms with unification resolution. The RUE theorem prover deduced the above refutation in 2.5 seconds using a total of 570 unifications. Typically a 9 step RUE proof will represent a fairly sophisticated axiomatic derivation which humans do not easily arrive at.

3. ~Comparative Analysis

In evaluating the performance of an automa ti.c theorem prover, it is always important to compare machine performance against human performance and in doing so to avoid extremes. We should not expect to capture in a computer algorithm the creative, analytical genius of an exceptional mathematician, rather we should be content to compare against astute human performance. We should require a theorem prover to prove theorems which astute humans find difficult to deduce. Since the reader will always consider himself an astute human, he can put the issue subjectively to test.

At this level of performance, automated deduction has important applications in many fields, including robotics, the science of intelligent machines, and also data base technology which should be more than sophisticated colle~tion schemes for explicitly stored data.

Since 1965 when resolution was introduced, we have accumulated substantial experience w.ith machine deduction by resolution. As recently as 1976, the Computer Transactions of the IEEE contained two important articles of major implementations of resolution theorem provers.

In the Maryland system of Wilson and Minker [5], the authors conclude with a very negative assessment of the efficacy of resolution:

"Considering that the average proof attempt using the best overall proof procedure required 42 CPU seconds, our results are discouraging. Even though most of the problems were relatively simple for a human to solve, the total CPU time required for the study cost more than $30,000. Clearly such a theorem proving system is far from practical. None of the inference systems tested enabled more than a marginal improvement in the overall power of unrestricted binary resolution. We have been unable to determine the problem and proof procedure characteristics which either enable problems to be solved or prevent them from being solved."

In contrast in the Argonne system of McCharen, Overbeek and Wos (6], the authors present 63 experiments ranging from trivial to quite difficult theorems, proven in diverse fields, together with some theorems in which their system failed. Their experiments represent one of the most successful attempts in automatic deduction. They presented for each experiment the input clause set used as well as a systematic tabulation of the amount of computation required. This paper in singular fashion established a benchmark for other researchers to compare with and we have here used it as a basis of evaluation of RUE.

We have conducted 17 experiments taken from MOW and dealing with Ring Theory, Group Theory and Boolean Algebra. The heuristic procedures developed from these experiments have, thus far, proven effective. We state the comparative results across 17 experiments between MOW and RUE in Table 1.

Notes on Table 1:

1. The RUE theorem prover was exceptionally superior throughout _the ten boolean and ring theory experiments, and in group theory both theorem provers achieved impressive results.
2. The RUE theorem prover was implemented in the PL/1 programming language and run on an Amdahl computer. The MOW theorem prover was implemented in Assembly language and run on the IBM System 370/195. It is difficult to compare runtimes in diverse hardware and sof_tware environments, and we suggest total unifications as a valid measure of comparison.
3. Since MOW used a complete set of equality axioms in the input clause set of all these experiments and since they do not tabulate anv

paramodulation counts, it seems that they made little successful use of paramodulation even though their paper states that this technique .-as incorporated in their system.

1. NPR: no published result without implying that MOW failed on these theorems.
2. MOW ran B4 and BS as a single theorem

which negated becomes a+ab1a v a(a+b)~a in the input ~lause set, and it is evident that the refutation of -(B4 ~ BS) is simply the concatenation of the refutations for -B4 and -BS individually taken and as derived by RUE.

1. The same holds for -(B6 A B7) whose proof is the concatenation of the RUE refutations for -B6 and -B7 individually taken.
2. In proving G3 and G6, the RUE ~heorem prover compared each new resolvent against each resolvent already in the refutation search tree in order to suppress duplicates and the overhead led to the very slow times 21 and 26 seconds. However, this duplicate removal can be implemented much more efficiently to reduce the runtimes considerably. For the most part, duplicate removal was not applied in the other RUE theorems of Table 1.

4. Experiments

The reader may wish to assess the difficulty of the above theorems by attempting their proof:

(4.1) Given the Boolean axioms

1. x+y ~ y+x

2. xy · yx

3. x+O = x

4. x*l = x

5. x+i · 1

6. x*x · 0

7. x(y+z) · xy+xz

8. x+yz · (x+y)(x+z)

prove the theorems:

Bl. 0. 1

B2. x+l ·1

B3. x*O - 0

B4. x+xy · x

B5. x(x+y) · X

B6. x+x · X

B7. x*x · x

(4.2) Given the axioms in Ring Theory

1. x+y - y+x

2. x+O · X

3. x+(-x) · 0

4. x(y+z) · xy+xz

5. (x+y)z · xz+yz

6. x+(y+z) · (x+y)+z

7. x(yz) · (xy)z

8 . x·y v x+z;y+z

prove the theorems:

R3. xy - (-x)(-y)

(4.3) Given the axioms of Group Theory

1. ex · x

2. xe = x

3. x-1x · e

4. xx-1 · e

5. x(yz) · (xy)z

prove the theorems:

Furthermore, with the reduced axioms set:

• (4.31) 1. ex · X 2. x-1x . e 3. x(yz) = (xy)z

With RUE a computer proved all of the above 17 theorems in 92 seconds which may be compared with the reader's own achievement. The brevity and incisiveness of the computer deduced RUE proofs (10] can also be compared with the reader's own humanly deduced proofs.

The above represent first experiments with RUE auto~ated deduction, wherein the longest theorem proven is 13 RUE steps (27 steps if using the equality axioms), and we will now outline the heuristics which were derived and employed in these first experiments.

5. Heuristic Principles Applied

The following are the principles which were experimentation: primary developed heuristic during

1. Heuristic ordering by degree of unification
2. Selection of the lowe~ level disagreement set not containing an irreducible literal
3. Heuristic substitution selection
4. Complexity bounds relating to:
5. (a) argument nesting
6. (b) number of distinct variables in a resolvent
7. (c) number of occurrences of the same constant or function symbol in a clause
8. (d) maximum number of literals in a clause
9. (e) maximum character length of a clause
10. Purging redundancies by subsumption
11. Demodulation
12. Frequency bounds for the use of individual axioms in a refutation path ~nd bounds on the consecutive use of the same axiom.

All nf the Ahove principles are syntactic in nature and apply generically to experiments performed. (1) through (3) ae RUE specific but the remaining principles have commonly been used by resolution theorem provers.

(5.1) Heuristic Ordering by Degree of Unification

If we wish to erase the literal t 1 ;t 2 , we measure the relevancy of an axiom a 1 · a 2 for this task by computing the degree of unification between complementary literals in the following manner:

1. Apply the MGPU to complementary literals to obtain ot 1 ;.,t 2 , oa 1 "'<7a 2
2. Set w·O (unification weight)
3. {3) For i·1,2

if oti matches oai identically

• then w · w+SO else if oai, oti are the same function, say

then w · w+20 and, furthermore, w · w+15 for each matching pair of corresponding arguments.

This is a simple scheme of matching which computes a weight of 100 when oa 1 -aa 2 erases ot1;ot2 and a weight of 0 when the complementary literals do not satisfy the equality restriction. There is also an intermediate scoring between these extremes.

For example, in the refutation of ab;ba stated in (2.1) which proves that a group is commutative if x*x · e, we used the input cla9se set:

Note that we have added to the input clause set the symmetry variant of each axiom which enables us in this experiment to build in symmetry without introducing the axiom x;y v y·x. This technique was also used by MOW.

Table 2 shows the unification scoring which took place for successive resolvents in the refutation of ab;ba. We place in parentheses axioms having a common score and * above the axiom ~ctually used in the refutation. We refer to txioms by their index in the input clause set.

The relative ranking of the refutation axiom in each scoring is given by the sequence: 3,5,2,1,6,2,4,1,1. The refutation axioms average to a relative position of 2.78 among 12 candidate axioms.

Furthermore, if we write the refutation as a weighted-axiom sequence:

we see that the minimum weight is 60 and that we may disregard an axiom scoring below 60 in the refutation search.

We may now state our heuristically ordering the refutation search tree: first principle of expansion of th~

1. Apply axioms to a negative literal in the order of higher degree of unificaion first and set a lower limit SDWMIN below which we suppress or postpone the application of an axiom (search directive weight minimum).
2. Furthermore, among axioms which qualify for application, select the first SDLIM candi­ dates (search directive limit)-.----

In reviewing all the refutations in group theory, we found tha SDWHIN 50 or 60 applied. Though the completeness theory specifies that all axioms for which w ) 0 must be used to preserve completeness, heuristically w )· 50 specifies a subspace of search where we should expect to find the refutation.

Furthermore, SDLIH specifies an inner-subspace of the latter which is even richer in expectation. In the Boolean Algebra and Ring Theory experiments, SDLIH 3 or 4 was successfully used.

(5.2) Selecting the Lowest Level Disagreement Set Not Containing an Irreducible Literal

Typically in adding the negated'theorem to the input clause set, we introduce skolem constants and when it is evident that these constants are in effect arbitrary constants with respect to the input axioms, then we can conclude that inequalities on skolem constants like a~b are irreducible, i.e. we cannot deduce a·b from the axiom set.

For example, in group theory the negated theorem ab~ba introduces skolem constants a,b, which with respect to the axioms:

are arbitrary constants and we cannot prove from these axioms that a·b. We should never generate an inequality alb in a disagreement set during a refytation search. Furthermore, inequalities like (a- a)b·e which demodulate to irreducible literals, are also irreducible and can never appear in a refutation.

This leads us to the following heuristic rule:

"In an RUE deduction, the disagreement

set likely to be required by a refuta-

tion, is the lowest l~vel disagreement

set not containing an irreducible literal."

In fact across 17 experiments containing 109 refutation steps, the above selection was always correct and what is more important led to proofs which did not require NRF.

The above rule heuristically complements the strict rule specified by the completeness theory where we state that we must select the topmost viable disagreement ~· which then requires us to descend to lower levels by NRF if necessary.

(5 . 3) Heuristic Substitution Selection

In the completeness analysis in [9], we establish that substitutions are to be performed only in variables at the first argument level of predicates in RUE and only in variables at the first argument level of the outermost function in NRF. This qualification of the HGPU is required for completeness. It leads, however, to proofs with extensive use of the NRF rule, yielding much longer refutations requiring deeper search trees. These same proofs can always be expressed in shorter form without NRF steps, by using immediate substitutions at lower argument levels.

Intuitively it is desirable . to use an unrestricted HGPU, achieving a maximum degree of unification so that inequalities in a disagreement set are reduced in number.

It in fact occurs in all 109 refutation steps in 17 experiments performed that maximum unification as described below is the refutation substitution:

1. First subsitute in a left-to-right scan only in variables at the first argument level.
2. Then in a second left-to-right scan, substitute in variables at all lower argument levels.

Let us unification refutation constants now apply both the notion of maximu~ and irreducible literals to our of ablba in group theory. From the

we define as irreducible literals:

and augment this set with demodulates to one of it~ demodulating substitutions any literal which members, using the

If in searching for a refutation of ab~ba, we heuristically choose the maximum unification HGPU and the lowest level disagreement set not containing an irreducible literal , we obtain the refutation we have already stated in (2.1). This proof which is specified by the heuristic theory is 9 steps compared to the 17 ·step refutation specified by the completeness theory which contains 8 additional NRF steps.

6. Completeness ~ Heuristic Theory

There is a polarity between completeness and heuristic theory, the latter tends to sacrifice completeness for the sake of efficiency which ~s crucial, and the former in giving the highest priority to the preservation of completeness tends to be seriously inefficient. It is important, however, to elaborate both approaches, and we have done this in [9] for completeness and here for heuristics.

7. Longest Experiment Performed

Let us now examine the longest refutation in Table 1, containing 13 RUE steps, which proves in ring theory that xy · (-x)(-y). The RUE theorem prover deduced this refutation · in less than 26 seconds employing 10,850 unifications in its heuristic search. The same proof with the equality txioms would be a 27 step refutation.

Substitution

The above refutation can be summarized as follows: "From the negated theorem ab f. (-a)(-b) and the axiom xfy v x+zf,y+z, form the construct

which factors to the form

Substitute -a/y and interpret as follows:

and we only need to prove -a(-b+b) · 0 which the refutation does as follows:

substitute -ay/z and factor

8. Conclusion

The above gives us a measure of the logical complexity of a 13 step RUE proof. We expect the current RUE theorem provr to be consistently effective in finding proofs of length 15, and we are now proceeding to attempt to prove very long theorems in the neighborhood of 40 steps, such as the following proven by HOW:

"In group theory, using the extended axiom set, prove

Using the equality axioms and lemmas the additional

HOW proved this theorem in 54 seconds using 184,955 unifications. Wos in [3] presented a 38 step paramodulation proof (humanly deduced) for this theorem without using additional lemmas. The RUE proof should be of the same length.

• If automatic deduction can be brought to be consistently successful in proving theorems such as the above, this will be a landmark achievement.

In the end there is an event which can serve to signal the maturity of automatic theorem proving, namely the appearance of controlled competitions (as in chess) between theorem provers and finally between machine and astute human.

• [1) Robinson, J. A., "A Machine Oriented Logic Based on the Resolution Principle", JACM 12, 23-41, 1965.
• [2) Wos, Lawrence, Robinson, G. A., Carson, D.F., "The Concept of Demodulation in Theorem Prov:ing", JACM, Vol. 14, No. 4, Oct. 1967.
• (3] Robinson, G. and Wos, L., "Paramodulation and ~beorem Proving in First Order Theories with Equality", Machine Ingelligence, Vol. 4, 1969.
• [41 Morris, J. · "!-resolution: An Extension of Resolution to Include the Equality Rela­ tion". Proc. IJCAI. 1969.
• [51 Wilson. G. A. · Minker. J. · "Resolution. Refinements. and Search Strategies: A Comparative Study" · IEEE Transactions on Computers. Vol. C-25. No. 8. Aug. 1976.
• Mc:Charen. Overbeek and Wos. "Problems and Experiments for and with Automated Theorem Proving Programs". IEEE Transactions on Computers. Vol. C-25. No. a. Aug. 1976.
• !71 Harrison. H. · Rubin. N. · "Another Generali­ zation of Resolution". JACM. Vol. 25. No. 3. July 1978.
• [8) Digricoli. V. J., "Resolution by Unification and Equality", Proceedings of the 4th Work­ shop on Automated Deduction. Univ. of Texas, Feb. 1979.
• [9) Digricoli. V. J. · "Automatic Deduction and Equality". Proceedings of the Oct. 1979 Annual Conference of the ACM. 240-250.
• [101 Digricoli. V. J. · "Resolution by Unification and Equality". Technical Report. Dept. of Computer Science. Courant Institute. New York University0 251 Mercer St ·· New York, N. Y. 10012. Sept. 1981. (The most complete refer­ ~ for .RUE theory and experiments).
• Wos. L., Overbeek. R., Henschen, L., "Hyperparamodulation: A Refinement of Paramodulation". 5th Conference on Automated Deduction, July, 1980.