The Management of Heuristic Search in Boolean Experiments with Rue Resolution

THE MANAGEMENT OF HEURISTIC SEARCH IN BOOLEAN EXPERIMENTS WITH RUE RESOLUTION

Vincent J . Digricoli

Hofstra University

166-ll 17th Road, Whitestone , N.Y . 11357

I RESOLUTION BY UNIFICATION AND EQUALITY

RUE resolution is equality-based binary resolution in that it incorporates the axioms of equality into the definition of resolution, making refutations less than half a s long as compared to using the equality axioms. Furthermore, it establi­ shes a context for heuristics leading to more efficient searches for proofs. RUE resolution is based on the following rule of inference:

l. RUE Rul e of Inference :

"The RUE resolvent of P(sl , .. , sn) v A and P(tl, ·· ,tn) v B, is dA v dB v D, where d is a Substitution and D is a disjunction of inequalities specified by a disagree­ ment set of the complementary_literals, oP(sl , .. ,sn) and dP(tl, .. , tn) ."

The above inference rule is in open form since we are free to choose the Sub­ stitution and disagreement set to be used . Let us now define the notion of a disagree­ ment set :

2 . Disagreement Set of a Pair of Terms :

"If s ,t are non-identical terms, the set of one element , the pair s :t, is the origin disagreement set . If s ,t have the form, f(al, .. ,ak),f( bl , .. , bk) , then the set of pairs of nonidentical, correspond­ ing arguments is the topmost disagreement set . Furthermore, if D is a disagreement set , then D' formed by replacing any mem­ ber of D by the elements of its disagree­ ment set , is also a disagreement set. If s ,t are identical terms , the empty set is the sole disagreement set ."

For example, the pair of terms:

f(a,h(b,g(c))) : f(b ,h(c, g(d))) has the

disagreement sets:

ABSTRACT

In assessing the power of a theorem prover, we should select a theorem diffi­ cult to prove, compare the quality of proof with the published work of mathema­ ticians, and most important determine whether cpu time used to find the proof is economically acceptable.

In this paper we apply the above cri­ teria to RUE resolution, equality-based binary resolution which incorporates the axioms of equality into the definition of resolution . We sel ect a theorem in Bool­ ean algebra, show the published proof of George and Garret Birkhoff s ide by side with the computer deduced proof achieved in less than 30 seconds of cpu time. The proof is quite long requiring the deriva­ tion of four lemmas and is proven by two RUE refutations of 16 and 18 steps respec­ tively . The same refutations with the equality axioms and unification resolution are 38 and more than 40 steps . Hence, the power of RUE resolution is shown by the brevity of proof compared to using the equality axioms .

The primary pragmatic issue in theo­ rem proving is the effective management of heuristic search to find proofs in accept­ able computer time. Whether an inference system Supports or obstructs this object­ ive is a crucial property and in this paper we explain in detail the heuristics applied to find proofs. These heur i stics are RUE specific and dependent, and can­ not be applied in the context of unifica­ tion resolut ion.

*This research was supported by a sabbatical grant from the IBM Systems Research Institute in New York .

Dl: ( f(a , h(b , g(c))) : f(b , h(c , g (d) ) ) }

D2 : ( a : b , h(b , g(c)) : h(c , g(d)) }

D3 :

D4 :

We now define a disagreement of compl e­ mentary literal s , P(sl , ·· , sn) ,P(tl , · · , tn) as the union: n

where Di is a disagreement set of the cor­ responding argument s si , ti . The_topmost disagreement set of P(sl, ·· , sn) , P(tl ·.. tn) is the set of pairs of corresponding argu­ ments which are not identical ,

Us ing the Substitutionaxiom for predicates, we can now state:

where D now represents a disjunction of inequalities specified by any disagreement set of P ,P . In reso l ut i on by unification and equality, we can resolve P and P im­ mediately to D. For example :

resolves in four distinct ways depending on our choice of D. We may resolve to f(a , h(b , g(c)))lf(b, h(c , g(d))) , to alb v blc v cld , or to an intermediate l evel D. These are logically distinct deductions since an input set may imply f(a , h(b , g (c)))=f(b, h(c , g(d))) without im­ plying a=b " b=c " c=d , so that the former participates in a refutation but the latter does not .

We now define a second inference rule s imilar to the above applying directly to an inequal;ity:

3 . NRF Rule of Inference:

"The NRF reso l vent of the clause tllt2 v A is dA v D, where d is a Substi­ tution and D is a disjunction of i nequal­ ities specified by a disagreement set of dtl , dt2 ."

For example we may deduce by NRF : f(a , h(b , g (c)))lf(b, h(c , g(d)))

or reduce to the inequalities of any dis­ a greement set . We call the above the Negative Re flexive Function rule .

In (Digricoli , 1983) we prove:

4. Completeness of RUE Reso l ution:

"If S is an E-unsatisfiable set of clauses , there exists an RUE- NRF deduction of the empty clause from S ."

This theorem establishes that resolving to inequalities is compl ete without intro­ ducing the axioms of equality(for Substi ­ tution , transitivity and reflexivity) or paramodulation . Apart from symmetry , the axioms of equality are applied implicitly by the RUE- NRF rules of inference .

We describe the a bove as completeness in ' open form ' s i nce we have not specified either the Substitution or disagreement set to be used . In (Digricoli , 1983), we deal with this issue and define the RUE unifier and the topmost viable disagree­ ment set as part of a completeness theory stated in strong form . However , in this paper we will use RUE r esolution in open form as defined above , heuristically ex­ ploiting this form and making effic i ency of proof search our primary goal .

II OUR PRIMARY EXPERIMENT

Our case study deals with proving the fol l owing theorem:

Given: the axioms of Boolean algebra :

1. X V y y V X

2 . X " y y " X

J , X V 0 X

4 . X " 1 X

5. X V X 1

6. X " X 0

?. x(yvz) xy v xz

8 . X V yz = ( xvy) ( xvz)

commutivity

di s t ributivity

Prove : x v (y v z) (X V y) V Z associativity of log ical or

This is a fairly complex theorem for a human to prove and we have the following proof published in the Transactions of the American Mathema tical Soc i ety [2] by George and Garret Birkhoff:

Theorem: a v ( b v c) (a V b) V C

Proof (Birkhoff):

We first prove lemmas: Ll, L2, L3 and L4.

Ll: a = aa since: a=al=a(ava)=aavaa =aavO = aa

L2 : ~a~v=l---=1 since: avl=(avlll=(a~l)(ava) =av(la)=ava=l

• L3: a = avab since: a=al=a(bvl)=abval =abva=avab

From lemmas Ll,L3,L4 and axiom 7, i t follows that:

Substitute the above for a,b,c in av(bvc):

On the right side, factor out the expression (avb)vc to the right:

av(bvc) = (av(bvc)) ((avb)vc),

On the right side , distribute (av(bvc)) across ((avb)vc) :

Applying Ll,L3,L4 and axiom 7 to each member of the right side, we obtain:

It is evident that especially the latter part of the above proof will be difficult for a human to deduce. In fact in human experiments with three mathemat­ ically astute university students, one could not prove associativity after six hours of work, a second proved associati­ vity in nine hours and the third proved the theorem in three hours. Hence, we are asking the RUE theorem prover to prove a theorem which humans find quite difficult.

The following is the proof deduced by the RUE theorem prover in 24 seconds of cpu time (IBM 370/3081), using a total~ unifications in its proof search, We first ask the theorem prover to prove two lemmas, xy v x = x and (x v y)x = x, and then augment the input axiom set with these lemmas to prove associativity.

2. Refutation to Prove: xy v x X

In the above refutation, we are uni­ formly applying the following Substitution:

"In a left-to-right scan of complemen­ tary literals, first unify at the highest argument level, and then in a second scan unify at all lower levels."

The refutation is a succinct 8 step RUE proof of the l emma , xy v x = x , and within this proof the sub- lemma, x v l = l , is proven beginning at step 4 . The same refutation performed with the equal ity axioms and standard unification resolution would be 19 steps .

J , Refutation to Prove : (x v y)x = x

We have a succinct RUE proof of ~ steps and an equival ent proof with the equality .axioms and unification resolution would be 19 steps . Note that the sublemma 0 = XAO is proven beginning at step 4 .

When the theorem prover is given the negated dual lemma :

it produced a 16 step refutation proving both l emmas in 1 . 4 seconds wi th a total 1485 unifications in the proof search . This refutation is s i mply the concatenat­ ion of the above two refutations and counting sublemmas , four lemmas are being proven in a singl e run of the theorem pro ­ ver . It corresponds to the work of the Birkhoff paper proving lemmas Ll , L2 , LJ , L4 and is a substantial piece of work .

4 , Refutation to Prove :

The 18 step refutation may be summarized as fol l ows :

suppose:

which completes the proof by contradict­ ion . We seethat the computer deduced proof is perhaps simpler and more elegant than that stated in the Birkhoff paper . The actual refutation is given in Appen­ dix I .

The theorem prover found the 18 step refutation proving associativity in 22 , 4 seconds using 6087 unifications in t~ proof search , An equivalent proof with the equality axioms and unification reso­ lution would be more than 40 steps . Alta ­ gether 2) , 8 seconds with 7572 unifications were used for the entire proof . Cpu time woul d be substantially reduced by a more efficient impl ementation of the theorem prover in assembl y language in place of PL/1 . This is a very fine result compared to other published work (McCharen , Over­ beek, Wos , 1976) and our purpose in this paper is to study the heuristic manage­ ment of proof search which led to the above result .

III FINDING A NEEDLE IN A HAYSTACK

Let us examine the enormity of the task of search which confronts a theorem prover seeking to find the refutations we we have stated . The difficulty of prov­ ing theorems in boolean algebra is com­ pounded by the commutivity of the boolean functions (v,A) and the symmetry of equal­ ity, so that the axiom x v 0 = x , has 4 variants based on these properties . We can incorporate the entire effect of com­ mutivity and symmetry by stating for the remaining boolean axioms all variants bas­ ed on these properties:

Hence , in boolean algebra we are really dealing with an input set of 144 axioms when we drop the axioms for boolean com­ mutivity and equality symmetry. Further­ more, the RUE inference rules implicitly incorporate the axioms of equality for substitution, transitivity and reflexivity and these axioms also do not appear in the input set , Let us assume that we will limit the input set to n clauses selected from the above variants: Let us assess the magnitude of search for the 18 step refutation which proves associativity when n is as low as 16 .

The theoremprover begins with the negated theorem with skolem constants, av(bvc) I (avb)vc , and must find the refu­ tation sequence we have stated . The refu­ tation search is represented by a tree :

Since in RUE resolution complementary literals always resolve, each of the 16 clauses in the input set resolves immedi­ ately with the inequality of the negated theorem and in a breadthfirst search 16 resolvents appear at level one of the search tree , The complete breadthfirst expansion of the search tree to level 18 has 16-to-18th leaf nodes , The situation is actually worse if we take into account resolving to different disagreement sets making the expansion factor at a node higher than 16 . Even with the input set reduced to 16 clauses, a breadthfirst search for a refutation is out of the question . The refutation we seek will be a linear input refutation represented by a path in the above tree . A miniscule number of paths from the root will culmin­ ate in the empty clause but at least one will when the input set is E-unsatisfiable.

We have stated that the refutation for associativity was actually attained by the RUE theorem prover in 6087 unifi­ cations, i.e . , the theoremprover heur­ istically developed a subtree of 6087 nodes in place of the breadthfirst expan­ sion . We wish now to explain precisely what heuristics were applied to define this subtree of search .

IV A HEURISTICALLY CONTROLLED PROOF SEARCH

In order to find a refutation in acceptable computer time , we must drasti­ cally prune the breadthfirst search tree and furthermore order the search in the remaining subtree . We will define the components of an evaluation function which heuristically determine which search paths to abort and what is the best leaf node to expand in the search tree. Furthermore , in applying an axiom to a node, we must heuristically select a disagreement set apt to participate in a refutation. The following principles were applied with these objectives in mind:

1. heuristic erdering by degree of unification,
2. selection of the lowest 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 clause
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. removing redundant resolvents ,
11. frequency bounds for the use of individual axioms in a ref. path,

All of the above principles are syn­ tactic in nature and apply generically to experiments performed. (l) through (J), which were crucial in our work, are RUE specific and cannot be applied in standard unification resolution with the equality axioms. The remaining principles have been commonly used in resolution theorem proving.

A. Heuristic Ordering by Degree of Unification

If we wish to erase the literal, tl I t2, in a refutation, we measure the relevancy of an axiom al = a2 by computing the degree of unification between literals as follows:

• (l) Apply the mgpu (the most general partial unifier) to complementary literals to obtain dtlldt2, dal=da2,
• Set w=O (unification weight).
• (J) For i = 1,2: if dti matches dai identically, then w = w+50, else if dti,dai are the same function, say: dti is f(bl,b2) and dai, f(cl,c2), then w = w+20 and, furthermore, w = w+l5 for each matehing pair of corresponding arguments.

This is a simple scheme of matehing which computes a weight of 100 when the mgu of complementary literals exists, and 0 when there is no degree of unification. There is also an intermediate secring be­ tween these extremes. We now state our first principle of heuristically erdering the expansion of the refutation search tree:

• (l) Apply axioms to a negative literal in the order of higher degree of unifi­ cation first and set a lower limit SDWMIN below which we suppress or postpone the application of an axiom (search directive weight minimum).
• Furthermore, among axioms which sat­ isfy SDWMIN, select the first SDLIM axioms with the highest unification scores (search directive limit).

The 18 step refutation for associa­ ti vi ty was .found using SDWMIN= 50, i. e., we pruned the search tree of all axioms falling below this unification score. In proving the supporting lemmas for associa­ tivity, all refutations were found using SDLIM=J, As naturally intuitive, this heuristic by degree of unification may be in RUE resolution, it, nonetheless, does not apply in unification resolution which requires the mgu at each deduction step.

B. Selecting the Lowest Level Disagreement Set not Containing an Irreducible Literal

Typically in adding the negated theo­ rem to the input clause set, we introduce skolem constants and when it is evident that these constants are in effect arbi­ trary constants in respect to the input axioms, then we can conclude that inequa­ lities on skolem constants like alb are irreducible, i.e., we cannot deduce a=b from the axiom set,

For example, the negated theorem, av(bvc)l(avb)vc, introduces skolem const­ ants a,b,c which in respect to the axioms of boolean algebra are arbitrary constants and we cannot prove two of these constants equal, Thus we should never generate an inequality like albinan RUE deduction. Furthermore, inequalities like (xvx)a I b which demodulate to irreducible literals are also irreducible and cannot appear in a refutation. This leads to the following heuristic rule:

"In an RUE deduction, choose as resolvent inequalities, the innermost inequalities not containing an irreducible literal."

Hence, in the refutation to prove xy v x = x, we resolved:

since resolving to bll would result in an irreducible literal. This heuristic prov­ ed successful, not only in all the boolean experiments, but also in ten experiments in group and ring theory (Digricoli, 1981). The RUE theoremprover permits the user to specify as input a list of irreducible literals, and, at the end of a run, it produces a list of ground literals present at leaf nodes of the search tree which the user may scan for irreducible literals in preparation for the next run.

c. Heuristic Substi tution Sel ecti on

In the compl eteness analysis i n (Digricoli , 1983) , we specify that Substi ­ tutions may be unconditional ly performed in variables at the first argument level , like P(x) , but only in variables at lower levels , like P(f(x) ), if certain condi­ tions are met by the input set . This leads to langer refutations requiri ng extensive use of the NRF rul e , when the same refutations can be stated in abbre­ viated form without the NRF rul e , i f we permit immediate Substitutions at lower argument levels . In fact , it occurs in experiments performed that the fo llowing maximum unification is the refutation Substitution:

"In a left- to - right scan of complementary literals , first unify at the highest argument level , and then in a second scan unify at all lower levels , "

Note that we have g i ven pri ority to substi ­ tuting at the first argument level as spe­ cifi ed by the compl eteness theory . Howev­ er , the above Substi tution selection which enhances t he effi ciency of finding proofs , is not universally compatible with RUE completeness and we show thi s in (Digri­ coli , 1983) .

V EXPERIMENTAL RESULTS

(1) Under l ength of proof , 5( 11) denotes that the 5 step RUE refutat ion is 11 steps when restated with the equali ty axioms and unification resolution .

(2) In Run 1 complexity bounds were appl ied wh ich perfectly fit the refuta­ tion derived , but i n Run 2 no compl exity bounds were appl ied to l imit search . Apart from this distinction , both Run 1 and 2 used the same input set and heur­ istics . In Run 2 of B5 , complexity bounds were relaxed one level and applied .

D. Pruni ng by Compl exi ty Bounds

An important method of pruni ng the search tree is to appl y compl exity bounds on reso l vents which are formed . Theorem provers working in areas of the search tree havi ng little relation to a refutation tend to produce resolvents which are too complex under a vari ety of attributes . The RUE theoremprover permits the user to specify complexity limits which when exceeded cause the resolvent to be discarded . These lim­ its relate to the depth of argument nesting, the character length of a clause , the num­ ber of l iterals in a clause , the frequency of appearance of a constant or function symbol in a c l ause (or l iteral) and the number of distinct variabl es in a c l ause . It is true that the ideal setting of com­ plexity bounds can only be derived by know­ ing a refutation . Nonetheless , it is im­ portant to know to what extent the proof search is contracted by applying complexity bounds . Experiments show that it is a good heuristic to use tight bounds to begin with (possibly derived from examini ng proofs in prior work with the theorem prover) and to gradua l l y relax these bounds . The experi ­ mental results in this paper are first sta­ ted by appl ying compl exity limits which are a profil e of t he refutation derived . We then suspend a ll use of these bounds , to determine the degradat i on of search which occurs. Both sets of results turn out to be favorabl e .

(J) To prove lemmas Bl through B4 , both individualy and altogether, the following input set was used :

A complete set of variants was used for the first four axioms but only a partial set for each of thedistributive axioms. In resolving with an inequality, the theorem prover first chose from each var­ iant set, that axiom having the highest unification score with the inequality. This reduced the applicable axioms from J2 to 6 , and of these only three with the highest unification scores were applied since SDLIM was set to J , This meant that the node expansion factor was J instead of J2 in the search tree and the excellence of the results in proving lemmas is due primarily to this heuristic tagether with avoidance of irreducible literals .

1. In proving B.5 associativity, we re­ duced the input set to 16 clauses and introduced variants of two proven lemmas:

1. X V 0 X 2, X X V 0 J . X II 1 X 4 . X = X II 1 .5 . X V X 1 6 . 1 X V x 7 . XII X 0 8 . 0 = X II X 9 . x(yvz) xy v xz 10. xy v xz x(yvz) lL (yvz)x yx v zx 12. yx v zx (yvz)x lJ. (yvx)x X lemma 14, X (yvx)x 1.5. yx V X X lemma

16. X yx V X

In this experiment, the theorem prover in reso l ving with an inequality chose only those input clauses whose unification score was .50 or greater (SDWMIN=.50) and SDLIM was not used. Our next experiments wil l attempt to prove associativity with­ out using l emmas and with the same input set of J2 clauses previously used. This will be an exceptionally lang refutation.

HEFERENCES

1. Digricoli , V,J ., "Resolution by Unifi ­ cation and Equality", Courant Institute, New York Univ., February 1983, (available through Univ . Microfilms).
2. Birkhoff George and Garret, "Distributive Postulates for Systems Like Boolean Algebra", Transactions of American Mathematical Soc iety, vol 60, July-Dec , 1946.
3. [J] Digricoli , V. J ., "The Efficacy of RUE Resolution: Experiments and Heuristic Theory" In Proc . IJCAI-8L Vancouver, B.C ., Canada , August 1981, pp . .539-547.
4. Digricoli , V. J ., "Automatie Deduction and Equality" In Proc . National ACM Conf ., Detroit, Michigan , October 1979, pp . 240-2_50 .
5. [.5] Morris , J ., "E-Resolution: an Extension of Resolution to Include the Equality Relation" In Proc . IJCAI-69.
6. McCharen , Overbeek and Was , "Problems and Experiments for Automated Theorem Proving", IEEE Transactions on Computers, C2.5-80, 1976.
7. Robinson, J .A., "A Machine Oriented Logic Basedon the Resolution Principle", JACM 12, 196.5, pp . 2J-41.
8. Brand , D. , "Proving Theorems with the Modification Method" , SIAM Journal of Computing, vol 4, no 4 , 197.5,
9. Harrison, M., and Rubin , N., "Another Generalizati.on of Resolution", JACM vol 2.5, no J , 1978.
10. Robinson, G., and Was , L., "Paramodulation and Theorem Proving" , Machine Intelligence , vol 4, 1969 .
11. Wos , Overbeek and Henschen, "Hyperparamodulation" In Proc · .5CAD, Les Ares , France , July 19~
12. Slagle, J ., "Automa tic Theorem Proving with Builtin Theories Including Eq . ", JACM, vol 19, no 1, January 1972.
13. [lJ] Shostak, R. , "An Algori thm for Reason­ ing about Equality" , CACM , vol 21, No 7, July 1978. --
14. *** Appendix I with the 18 step refutation proving associativity has been omitted due to space limitations. This refu­ tation will be given at the conference presentation.