A Hole in Goal Trees: Some Guidance from Resolution Theory

1. Introduction

After several years when almo s t all theorem prov­ ing systems, and many problem solving systems, were based on resolution, many researchers are returning to natural deduction type logics, often implemented via some form of goal-subgoal tree notation using a prob­ lem reduction approach. In thi s paper the goal-sub­ goal tree form (or AND/OR tree form) is cons idered. We show tha·t if one wishes to use thi s syntactic form for representation of the deductions and search space as a full replacement for the resolution approach, one must make some additions to the classical problem re­

duction formulation.

To show that there exi s t holes in the classical goal-subgoal problem reduction method we need only present some examples, which we supply. To determine an appropriate correction and mea sure its power takes some theory. It turns out that resolution theory, in particular the model elimination procedure results, provides an adequate theoretical base. In this paper we only state the consequences for the problem reduc­ tion approach, omitting proofs. However, we want to stress the value of resolution theory for the insight it gives to the problem reduction method and remark that more information than is exploited here can cer­ tainly be pulled from existing resolution theory .

AND/OR trees , us ed as goal trees , are component s of most problem solving systems that are not resolu­ tion based. We are hereafter concerned only with goal trees used for logical inference. We show, among other things, that the usual way of organizing goal ­ subgoal trees i s incomplete yet one small change makes the mechanism complete, a ssuming equality sub s titution is not relevant, and if the equality predicate is used, several added rules gives completeness in general. By completeness, we mean that the goal trees and a ssoci­ ated syntactic mechanism is capable of establishing a goal statement whenever the goal is va lid given the assertions present. The systems we discuss are the search trees such as are us ed in the Geometry Theorem Machine (Gelernter et al.2,3,4), the Logic Theorist (Newell et al. 12 ) and elsewhere. Indeed, when the equality predicate is not present, the mechani sm of the

Plane Geometry Machine is suffi cient in structure and and examp l e .

t Research supported in part by NSF Grant GJ-28457X1 .

1< Present address: Computer Science Department, Duke University, Durham, N. C. 2770U.

Let us represent our syntactic, or semantic , atoms by capital Latin letter s : A, B, C, ··· ,with sub­ scripts if necessary. Of cour se , A may be a complex formula, e.g., (Yy)(Yx)P(x , y) ~ Q(y ) , but we agree not to consider it s interior structure relevant to the par­ ticular problem so it is "packaged" as A, We consider our pr ima r y , or !££, goal G to be the atom to be es ­ tabl ished. Assert ions (fa c t s) are of the form A 1 A .·· AAn ~ C (impl ications) or P (premises) . The A. are antecedent s and C is the consequent of the impli~a­ tion. For notational convenience , we define the conse­ quent of a premise to be the premise itself and the set of antecedent s of a premise to be the empty set . For a parti cular prob lem we begin wi th a goa l to be estab­ lished and a set of assertions . We consider the ex­ pression format more closely later.

A goal tree records the development of the search to establish G by l inking it to the premises via t he implications. G is the top goal; if i t is a l so a premise, G is established. Otherwise al l impl ications with consequent G are located and the antecedents of each such implication become new goa l s , subgoal s of G. G is the parent of each new goal a nd each new goa l is the successor of G. If each new goa l for one of the implications can be es tab l ished , G is then es tabli shed (by asserting the implication) . The antecedents of one implication f orm partner goa l s . We also r efer to a conjunction of goa l s ·meaning the se t of antecedents f rom one implication. Any single set of partner goals (goa l s in conjunction) at this level that can be es ­ tabl ished e s tablishes G. This y ields a di s junction of partner goal sets . If no partner goa l se t correspond s to a set of premises, some partner goal set is selec t­ ed and each of the partners not a premise is again matched against implication conclu s ions to crea te (pos ­ s ibly) new subgoa l se t s (not necessarily as a single parallel act ion) . This proceeds in iteration until a sufficient set of premise ma tche s are found, or the search s tops . The conjunct ion/ di sjunction relation­ ship above leads to the name AND/OR tree .

A goal A is an ancestor of goal B if A i s the parent of B or A is an ances tor of the parent of B. A partner of an ancestor of the goa l A is called an ances tor partner of A.

We give an elementary example from pl ane geometry in the spirit of the Geometry Theorem Machine (GTM); see Figure 1. Immediate subgoals lie below their goa l and are connected by a slanted l ine . Par tner goa l s are connected by a hori zontal line. In Figure 1 the bot ­ tom leftmost conjunction of goa l s is rejected even though two goal s are premi ses becau se the third goal a l so oc cur s as t he top goa l, thus it is an ancestor of itself. Any goal that occurred as an ancestor goa l of itself was rejected at the lower level i n the GTM s tructure because if it cou ld be established at a ll, i t could be es t ab li shed f rom the higher l evel. Also in the GTM s tructure was a way of discarding a con­ junc t ion of goals if a higher conjunction containing an ance s tor wa s easier to prove . We do not e l abor ate for we handle this somewha t differently . The key point i s that interaction with ancestor goa l s existed , and was ve r y important due to the "depth first" search whi ch meant not l eaving a branch until you could go no further .

We now enl arge our for~at fo r expressions . This is done by al lowing our a toms t o be literal s , atoms possibly pr eceded by a negation sign~ Thu s if A is a complex expression, we look inside onl y to check if the l ef tmost symbol is "- "not" operator of proposi tion­ a l logic . If so , it is displayed. We l et A, B, c, ...

(possibly with subscripts ) repre sent literal s . To emphasize tha t B is A proceeded by a "not" we will sometimes write B as ~. A a nd -A are complement lit­ erals. Otherwise, our expression format is as before.

The use of negated goals ha s not appeared in the clas sical inference programs u sing goal - subgoal sys ­ t ems . The Geometry Theorem Machine avoided the nee-d to recognize complementary goal s almost by accident, for concep t s like "XYZ is collinear" and "XYZ is not col­ l inear" both appeared but di d not interact. However, in genera l si tuations particularly in robot sys tems, question answerer sys tems , etc. interaction between complementary literals is to be expec ted. Certain re­ cent systems of a goal - subgoal format have been de­ signed to handl e negated formulas so tha t complemented l i t era l s i nt eract; see Bledsoe et al. 1, Reiter15 The se sys tems are l ess in the classical goal" - subgoal fo rmat than the sys tem considered here and also appear to be incomplete .

We consider i n Figure 2 a s i mple example in which the goa l follows from the assertions but the goal-sub­ goa l mechanism so far illustrated will not e s tabli sh the goa l. One rea son is that the contrapositive of one of the assertions is needed. We add the contrapos­ i tive as an explici t as sertion. We not e , however, that there is no way of proceeding to a premise! Ye t the problem is simp le enough so that one can read the in­ tended meaning of the assertions and see that the goal follows . We claim that because~ occurs as an (indir ­ ec t ) subgoal of C, we can trea t ~ as if it were a premise and terminat e that branch . That i s , ~ is now marked contradicted and conside r ed established. As A is a premise, B i s established, so C i s es tablished, as desir ed ,

The rationale for the mechanism above is not hard to find. Ei ther C is true or~ is true. If ~ i s true , then we can es tablish C (after establishing other pertinent subgoals), which is impossible. Thus C i s true. This is an argument by contradiction. We ob­ serve that the check for thi s is trivial if possible identi t y with ance s t or goal s i s checked as in the GTM . One simply checks for ident i ty and then complementa ­ tion.

The not-so-immediate fact is that we now have a prepositionally complete system. That is, if no sub­ stitution i nside literals i s allowed so as to make dis­ tinct l iteral s alike (or complementary) no further gimmicks will be necessary . In Figure 2, we not e a possible alternate argument to produce establishment is that one of D and -D is true so one of the t wo ways of es tabl ishing C should be permi tted. Is this suffi­ cient also? Probably so , we are not sure. In any event, it is generally a much more difficult check as the occurrences of D and -D are on different di sj unc ­ tive branches and can be made to appear at an arbitrary depth by making the inference connecting C and D more comp l ex . Thus instead of a nearly free check one has a relative ly complex tree search. But might such a tree sea r ch be necessar y anyway , for some case where ance s tor complements do not occur? No. That is the meaning of our s tatement that the sys tem is now prep­ ositionally complete . The proof is a consequence of the completeness of model elimination (ME) .

In general, problem solver s will not be constrained to work preposi tionally. The expressions we have con­ sidered , goa l and a ssertions , will in general have free variables and functions, including Skolem functions which build in universal quant ifier s . We do not con­ sider in detail the process of general conversion to our chosen format (generalized somewhat below). It is basically the conver s ion to disjunctive normal form with Skolem functions, the dual to the "conversion" in Nilsson13, for example . The general structure of t he goal-subgoal mechanism when operating in the presence of free (individual) variables and substitution is the same but with direct comparison replaced by the notion of unif~Sation from resolution (see Robinson17, Nilsson , or Slagle 1 9).

One of the common substitution situations involves equality. If we have goal P(a) and assertion a=b we certainly consider P(b) a subgoal whose establishment would yield P(a) . Indeed, some readers may wonder why we need to write P(b) explicitly . P(a) might be inter­ preted as all statements equivalent to P(a) under equality substitution. This has disadvantages when substitutions use numerous derived equations so we re­ ject this here although a use of such identification might be satisfactory . Such a treatment is compatible with our main points but requires a modified organiza ­ tion to that given below.

In Figures 3, 4, and 5 we give examples where the goal should be inferred from the assertions presented but cannot be inferred under the simp l e format of the preceding paragraph. These figures suggest the format in which we propose to handle such problems . That is, in our general description below the problems stated would generate the goal tree presented. Note that in Figure 4 an alternate form of implication 1 is needed . We supply it here as assertion 4. We call 4 a general contrapositive of 1. We remark that we would expect the situation of Figure 4 to arise very infrequently so such an inference route should be investigated only when desperate.

Again, if we adopt the few rules for handling equality given below, of which three instances have been displayed, we have completeness of the goal tree procedure when equal ity substitution is included. The completeness proof comes from the appropriate form of ME with paramodulation (an equality handling mechanism) whose proof appears in Loveland11.

A number of other features for goal tree analysis can be gleaned from resul ts concerning ME . Most are natural in this setting such as the removal of a con ­ junction of goals when one goal matches an ancestor goal. We noted this was incorporated in the GTM. A non-intuitive situation is that a conjunction of goals can be eliminated if one of the component goals is complementary to an unexpanded ancestor partner goal, i.e., a goal with no subgoals yet recorded, but com­ pleteness is not assured unless a goal is marked dis ­ placed, and treated as established, whenever it match­ es an unexpanded partner or an unexpanded ancestor partner goal. Displacement is illustrated in Figure 6. Displacement avoids expanding the same subgoal twice.

Figure 7 is an example of another situation we must handle . If S is an unsatisfiable formula, S ~ C is valid for any formula C. We use the device of the contradictory formula i, which may be considered a shorthand for formula P A ~P. This device allows a natural extension of our notion of assertion and goal and suffices to handle cases where the goal, or sub ­ goal, cannot be directly derived although it is a valid consequence of the assertions .

We write the general format for our goal tree system as if a propositional system is our concern. That is, all comparisons of literals are by identity or complementarity. However, the word matches is used for this identity check. By interpreting matches as using a most general unifying substitution, the general form is realized when substitution for (individual) free variables is permitted. We include in our forma t the substitution of equality but, again, with the ambi­ guity which may or may not allow free variables in those terms .

For convenience we label the problem reduction procedure below the MESON (~odel Elimination ~ubgoal Qrie~ted) procedure .

We consider again the expression format. An arbi­ trary first order formula can be converted to the ap­ propriate expression format, preserving validity. A formula, or (finite) set of formulas, not already suit­ ably expressed should be converted to the following form:

where B. is of the form A 1 A .· . AAm ~Cor C and G is of the fo~ L 1 A . ·. ALk' where the A.'s, L. 'sand Care lit­ erals . Th~s is readily obtained from~the disjunctive normal form of the original formula. G then defines the goal: if K=1, L 1 is the single goal, otherwise L 1 , .·· , L are top level partner goals all of which must be eventhally established. We can tackle one at a time (though they may be linked by common variables) so hereafter we consider a single goal G. A 1 A . . · AAm ~ C is an assertion implication, and C a prem~se . An im­ portant equivalence for format preparation is (A~ B V C) : (A A -B ~C) . This is used to form the various general contrapositives needed for complete­ ness . We extend this to generate ~ ~ i from A, for example.

If the goal is believed to follow directly from the assertions (as is usually the case) the use of i may be avoided. Otherwise, add i ~ G, the assertion generated from the goal, to the assertions and for each a s sertion A 1 A · · . AA ~ C add the general contrapositive A 1 A ·· · AAm A~~ i~ and for each premise add~~ i . Only one such formula need be added to the assertion list if some version of that assertion is believed necessary to establish the result .

It is necessary to consider, for each assertion implication A 1 A ··· AA ~ C, m general contrapositives plus the orig~nal as~ertion if completeness is to be preserved. There should be one general contrapositive A 1 A ··· Ai-l A~ A Ai+ 1 ·· . A Am~ ~i fo: e~ch i. _The order or antecedents ~n any assert~on ~s ~mmater~al .

3. The MESON Procedures

The procedures presented here are for proposition­ al (variable free) problems. We will make occasional reference to the requirements of the procedures utiliz ­ ing variables.

The procedures represent syntactic systems for adding to a goal tree information about goal-subgoal relationships and establishment of goals. The proce­ dures return "success" or "failure" according to wheth­ er the top goal can be established or not respectively. Of course, the ability to return "failure" disappears when substitution is allowed, e . g . , first -order formu­ lations. A returned value of "failure" for a problem indicates either the top goal does not follow from the assertions or the search ordering and goal generation and deletion strategies specified by the planning rou­ tine are inadequate for the problem. (It is possible to write a complete planning routine which theoretic­ ally always returns "success" for soluable problems.)

We will now present two MESON procedures for goal tree analysis incorporating the new rules discussed above . The procedures are logically di vided into four subprocedure s with label s "initialize", "loop", "up­ date_marks" and "update_goal s".

The instructions placed at the labe l "initialize" define GOALS ( the se t of goal s to be att empted) to be the set consisting of only the top goal and also ini­ tialize the goal tree.

The instructions placed at the label "loop" sel ect a goal G from GOALS, an operation to be performed and an assertion D if needed. The selected operation is then performed for the goa l G and assertion D. Those operations try to establish goa ls or create subgoals .

The instructions placed at the label "update marks" mark a goal "estab li shed" if each of a list of partner successors is marked "established", " contra­ dicted" or "displaced". Thus, if each of a conjunc­ tion set of subgoals of a goal is established , the goal is established.

The instructions placed at the label "update goals" add newly generated subgoals to the tree a;d GOALS provided certain acceptance criteria are met.

The selection of the nex t goal in GOALS to be operated upon and the se lection of the operation and the assertion to be used in operating on that goal are assumed to be accompli shed by some externally speci ­ fied planning routine ("the planner" ) . The planner, in addition to specifying a search s trategy , may re­ strict or totally eliminate use of some of the opera­ tions. For example, traditional goal tree procedures without the contradiction mechanism correspond to a planner which never uses the operation at "op3".

The planner, by applying the operation at "op5" to a goal, r emoves the goal from GOALS and thereby signifies that no more operations will be applied to the goal.

If one wishes to insure completeness, the planner must in some order proces s all operations (except the operation at "op5" ) for each goal and potentially ap­ plicable assertion. The planner may select the goals of a conjunctive set of goals in any desired order to attempt their establishment . The procedure(s) make no assumption as to whether the search is depth - fir s t, breadth-first, or some mixture of the se .

MESON procedure

initialize: Let GOALS be a set consisting of only the top goal. Initialize the goal tree to the top goal.

loop :

If GOALS is empty, exit procedure with "failure". Let G be a goal in GOALS selected by the planner . The planner selects one of the following operations to be performed on G and selects D, a premise, implication or general contra­ posi tive of implication, as required by the operation.

op1: If G matches the premise D, mark G "established" and go to update_marks. Otherwise go to loop .

op2: If G matches the consequent of D, where D is an implication or general contra­ positive of implication, let A be the set of the antecedents of D and go to update_goals. Otherwise go to loop.

op3: If G matches the tor of G, mark G to update_marks. complement of an ances ­ "contradicted" and go Otherwise go to loop.

op4: If G matches an unexpanded partner of G not marked "displaced" or an unexpanded ancestor pa rtner of G, mark G "di sp laced" and go to update_marks . Otherwise go to loop.

op5: Delete G from GOALS and go to loop.

update_marks: If G is top goal, exit procedure with "success". If all partner goals of G are marked "established", "contradicted" or "displaced", let G 1 be the parent of G, set G=G 1 , mark G "establi shed" and go to update_marks . Otherwise go to loop.

update_goals:

tes t 1: If a member of A is identical to G or an ancestor of G, go to loop.

test 2:

I f a member of A is complementary to another member of A, a partner of G or an ancestor partner of G, go to loop.

Otherwise add the members of A to GOALS and to the goal tree as a conjunctive se t of successors of G and go to loop .

The MESON procedure for equality incorporates rules for handling the equality relation. It differs from the MESON procedure in that three new operations are added. Also, the rules for disregarding newly gen­ erated subgoals (at "test 1" and "tes t 2") have not been proven to preserve completeness although we be­ lieve completeness is preserved with these rule s ap­ plied. We maintain the update_goals subprocedure in the MESON procedure for equality with the admonition that if completeness is to be preserved these rules shou ld be bypassed (at present) .

For technical reasons , it is necessary to put in premises of the form a=a for each term a or, if in a setting using free variables and substitutions, one must put in x=x and f(x 1 , · · · ,x) = f(x 1 , ·· · ,x) for each n-ary function symbol f . nSuch axloms cag be re­ placed by appropriate procedure rules if desired.

MESON procedure with equality

initialize:

(same as for MESON procedure)

loop:

(preface and operations 1-5 same as for MESON procedure; only change is the ad­ dition of the following operations)

op6: If G contains a term matching term a where a=b or b=a is the consequent of D, where D is a premise, implication or general contrapositive of implication, let A be the set consisting of G with a s ingle instance of a replaced by b plus the antecedents of D and go to update_ goals . Otherwise go to loop.

op7: If the consequent of D, where D is a premise, implication or general contra­ positive of implication contains a term matching term a where G is afb or bfa, let A be the set consisting of the

complemented consequent of D with a single instance of a replaced by b plus the antecedents of D and go to update_ goals. Otherwise go to loop.

op8: If H is an ancestor of G or G itself and H (resp. G) contains a term ma tching term a where G (resp. H) is atb or bfa, let A be the set consisting of H (resp . G) with a single instance of a replaced by b and go to update_goals. Otherwise go to loop.

(Note: see examples below. )

update_marks:

update_goals:

(same as for MESON procedure)

(same as for MESON procedure)

We attempt to clarify op8 and shed light on its usefulness. Consider the case that H is G and G is afb, a and b simple constants . Then, reading the "respectively" case , we see that G contains term a and H i s atb. Then A, the possible new subgoa l, is G with replacement, i .e., bfb. Taking the other case (ignor­ ing the "respective ly") yields the same possib le sub ­ goal. This is certainly unproductive and could actu­ ally be deleted with no ri sk involved. However, in a free variable setting with substitution it is important. Suppose the goal is f(x)tx and the sole premise is f(f(x))fx. By op8 where H is G is f(x)tx, ignoring the respectively's (for variation), we have H contain­ ing a term x matching f(y), under substitution f(y ) for x, where G is f(y)fy (the change of variable name is a necessary detail ); now atb is f(y)fy. Then A consists of H with replacement, i.e., f(f(y))fy . This subgoal matches the premise and the desired result is obtained.

It is impossible to give an adequate discussion within thi s paper of the modifications required to handle first order formulas, i.e., allowing quantifica­ tion of individual variables in the problem s tatement. This is best done elsewhere where space permits a full discussion. The modifications are generally s traight­ forward if the reader is familiar with resolution theory, in particular ME . See Loveland11. Subtle point s do arise, however, as suggested below.

Performing matching by u·se of the general unifica­ tion algorithm i s an important idea and, although we can conceive of reasons to select les s general substi­ tutions under certain conditions, the advantages of obtaining the most general substitution should not be given up lightly. This is an important aspect where knowledge from resolution theory can enhance the prob­ lem reduction method .

We make two further points, really warnings , con­ cerning adopting the above description of the MESON procedure to first order expressions . If the goal has a free variab le in it, the negation of the goal shou ld be made a (hypothetical) premise. To see this, con­ sider the following example: Goal: P(y) (i.e., we want to know if ~yP(y)) . Assertion: ~P(f(a)) ~ P(a) . Clearly either P(a) or P(f(a)) holds . We need ~P(x) as a premise to realize thi s . A second point: a sub­ stitution may occur in a subgoal when applying an as­ sertion implication. This substitution must be made at each occurreuce of the replaced variab1e tqrough­ out the goal tree. Thus copies of the goal tree must be retained in .such instances for back up in case of failure . A good format for handling this involves adopting the ME format to the MESON procedure organiza­ tion.

4 . Conclusion

This paper can be read simply for the illustra ­ tions of possible extensions for the problem reduction method. However, we have attempted to convey inform­ ally that resolution theory can contribute to the under­ standing of alternate syntactic methods . Other devices of resolution such as linear representation of goal trees and use of unit clauses from premises may also be of use. We do believe that the MESON format , which simpl y extends classical goal tree representation, may present a very useful way of incorporating resolution ideas in future problem so lving programs.