Proving the Impossible is Impossible is Possible: Disproofs Based on Hereditary Partitions

1 . Introduction.

Theorem proving a nd problem solving programs are some­ times successful in 1inding a proof to an actual the­ orem, or in solving a problem which does have a solu­ tion. On the other hand, presented with an expression which is not a theorem, or with an unsolvable problem, the programs are generally incapable of discovering, in a positive sense, that the expression is not a the­ orem, or that the problem is indeed unsolvable. The usual diagnostic would be: "I cannot solve the prob­ lem, because my resources are exhausted, or because I am stuck somewhere . However, the problem~ be solva ­ ble. I just don't know."

We are interested in developing programs which, given a problem, will try to solve it . If they cannot solve the problem, they will try to show that it cannot be solved. A program which performs the last function will be called a disproving program . To build such programs, we use a technique which we named hereditary partitions. This technique has some generality and forms our basis for a program, DISPROVER, which has been applied to disprove goals in robot worlds, i.e. DISPROVER proves rigorously that, for a given set of axioms, operators and an initial world, there is abso­ lutely no way to attain some particular goal.

DISPROVER also cooperates with another program, LAWALY, which tries to find paths to goal states. Sometimes, when LAWALY cannot solve a (solvable) problem, DIS ­ PROVER -which clearly cannot disprove the solvable problem- gives LAWALY additional information which per­

mits a solution to be found .

We shall now describe some additional motivation for our work, discuss the related technique of hereditary properties -which is a degenerate case of hereditary partitions- and give several examples of disproofs, terminating with examples of cooperation between DIS­ PROVER and LAWALY.

2. Why Disproofs?

Somehow, it is much more romantic and challenging to show that, in the whole wide world, there is absolute ­ l y no way that something can be proved, than to find one, of possibly many, proofs to some theorem. More­ over, work on robots introduces a practical -and neces­ sary- application of disproving programs. In robot problem solving s ystems, parts of the physical world, including some of the robot's capabilities, are simu­ lated as a model. It is desirable that the model con­ form reasonably closely to the physical world, other­ wise the robot may "think" that it can do some things

*Work partially supported by grant GJ - 34736 from the National Science Foundation.

PROVING THE IMPOSSIBLE IS IMPOSSIBLE IS POSSIBLE: DISPROOFS BASED ON HEREDITARY PARTITIONS*

I

L . Siklossy and J. Roach

Department of Computer Sciences

Uni versity of Texas, Austin, U.S.A.

-which are in fact impossible- or cannot do some other things -which are in fact possible-. For example, in [1], the robot can be in two different places at the s ame time~,3

3. Some Techniques for Disproofs.

Many systems of interest, such as predicate calculus, are undecidable, i.e . for a given statement in the sys­ tem it is not possible to determine, in general, whether a given statement in the system can or cannot be proved. If, in a particu}ar case, we wish to show that a state­ ment is not a consequence of some axioms, the standard procedure is as follows : find a model in which the axioms are true, but the statement is known to be false. Such model building is truly an art, and is acquired through much experience. The automatic building of dis­ proving models appears beyond the present state of the

art .

Since predicate calculus has been of great interest to workers in artificial intelligence, some additional comments are in order. Given a well - formed formula wff in predicate calculus, three exclusive cases are possible:

1. wff is a theorem .
2. ~wff is a theorem.
3. neither a) or b). In this case, ,wff is also in category c). This last case is by far the most common, in the sense that, given a finite vocabulary of con­ stants, variables, function and predicate names, the number of well-formed formulae of a given length in category c) far surpasses the number of formulae in categories a) and b) .

Given a wff in categories a) or b), a theorem prover based on resolution, for example, can determine after a finite time -which, in general, cannot be calculated in advance - in wh i ch of the two categories the wff be ­ longs . To obtain this result, the theorem prover could time-share its effor ts between trying to prove the in­ consistencies of both wff and iwff. However, i f the wff is in category c), then usual l y the theorem prover will go on forever. In only very few cases will the theorem prover stop because no new clauses are genera ­ ted: a disproof of the wff has then been obtained .

A disproving program in predicate calculus would at­ tempt to determine that a wff is not in category a). The above discussion shows that present theorem provers are at best very weak disproving programs.

It should also be noticed that a proof of the attaina­ bility of the negation of a statement does not imply that the statement itself can be disproved. For exam­ ple, if a light can be turned on and off (at different times) then the statement STATUS(LIGHT ON) and its ne ga­ tion , sTATUS(LIGHT ON) are both attainable, and hence neither can be disproved. ·

While t he theorem proving approach gives results in far too few cases, and model building is too often ad -hoc, a disproving technique with some generality has been called hereditary properties (see [4] for some examples). Consider a checkerboard from which we remove two oppo­ site squares. This mutilated checkerboard cannot be covered by dominoes. To obtain a disproof, we notice that whenever we add another domino on the checker­ board, the number of white and black squares that have been covered remains the same. This property -the equality between the number of black and white squares that have been covered- is hereditary, that is it does not change as ~ allowable move -putting a domino on the checkerboard- is performed. The disproo f is com­ plete when we notice that, in the mutilated checker­ board, the number of black squares does not equal the number of white squares, (the difference is two . )

The technique of heredit ar y properties can be summa­ rized as follows:

-the original state(s) of the model has (have ) some property.

-whenever a state has this property , all states ob­ tained from it by all allowable moves still have this property.

-the goal state which we are trying to a ttain does not have this property.

Hence the goa l is unatt ainable. W.W.W. (what we want­ ed ! )

4 . Hereditar y Partitions .

Hereditary partitions generalize the basic idea of hereditary properties . The technique of hereditary partitions can be summarized as follows:

-call the set of all states that can be achieved from the original state(s) by all lega l sequences of moves the attainable world.

- the attainable world can be partitioned into disjoint partitions. Hence each original state is in some par­ tition.

- the goal state which we are trying to attain does not belong to any of the partitions. Hence the goa l is unattainable .

Obviously, hereditary properties correspond to the case where there is only one partition .

We notice that if we apply a lega l move to a state in some partition, we obtain a state in the same or some other partition . We can say that partitions are closed under lega l moves . In fact, as long as this closure property is maintained, we might just as well add to the partitions some unatt ainable states (i.e. states which are "meaningless") if that makes life simpler . Even further, to the partitions containing some · attain­ able stetes we can add some partitions containing no attainable states. The disproof is still complete if this expanded set of partitions is closed under lega l moves -i.e. from one partition in the set any legal move leads us to the same or some other partition in the set - and if the goal state that we are trying to disprove is not in any of the partitions.

In practice, the problem is, of course, to build the appropriate partitions . We shall see an example in the next section .

5. Example of a Disproof using Hereditary Partitions.

We shall consider robot worlds axiomatized in a manner similar to that used in [1]. The world is described as a set of predicates, for example NEXTTO(ROBOT BOX2). Moves in the world are operators which must satisfy some preconditions, and their effect on the world is specified by a delete set and an add set .

Let us consider a subworld of the world in [1]: a ro­ bot and three boxes, BOXl, BOX2 and BOX3, in a room. The only relevant operators for our problem are (some­ what simplified from [1]).

goto(object), meaning: robot goes next to an object. Preconditions : ONFLOOR .

Delete set: ATROBOT($) NEXTTO(ROBOT $)>~.

Add set: NEXTTO(ROBOT object).

push(objectl object2), meaning : robot pushes objectl next to object2.

Preconditions: PUSHABLE(objectl) A ONFLOOR A NEXTTO (ROBOT objectl) .

*$ means every thing . At least that was the meaning before a series of deva luations!

Delete set : ATROBOT($) AT(objectl $) NEXTTO(ROBOT $) N EXTTO(objectl $) NEXTTO($ objectl).

Add set : NEXTTO(objectl object2) NEXTTO(object2 ob ­ jectl) NEXTTO(ROBOT objectl) .

We assume that boxes are PUSHABLE, that the robot could climb on and off boxes, and possibly do a ·lot of other mischievous actions, none of which would help her get two boxes next to each other. We now wish to solve the problem: get the three boxes next to each other, i.e. find a path from an original world which includes: ONFLOOR ATROBOT(A) AT(BOXl Al) AT(BOX2 A2) AT(BOX3 A3)

to a goal state which includes:

NEXTTO(BOXl BOX2) NEXTTO(BOX2 BOX3).

A solution is: goto(BOXl), push(BOXl BOX2), goto(BOX3), push(BOX3 BOX2).

However, a more symmetric description of the ·goal state answering the statement "the three boxes are next to each other" would be:

NEXTTO(BOXl BOX2) NEXTTO(BOX2 BOX3) NEXTTO(BOX3 BOXl). We shall now give a disproof of this goal, i.e. show tha t it cannot be achieved.

The partitions are described in terms of some anchor predicates and their negations. As a first choice, DISPROVER chooses the three predicates from the goal as anchors . We shall abbreviate these predic ates as Pl2, P23 and P31. The original state belongs to the parti ­ tion :

Partitionl: 1Pl2 II ll'23 fl iP3l.

This partition contains all states, whether attainable or not, which satisfy 1Pl2 f\ 1P23 and 1\ ·P3l, i.e. which do not contain any predicate of the form: NEXTTO(BOXi, BOXi(mod 3 )+l)' i = 1,2,3 .

If the robot could juggle she would move into a new state which would presumably still be in the partition. All goto operations do not, in turn, make her go out of the partition. But let us consider: push(BOXl BOX2). This operator is applicable to partitionl -although not to the original world, because the robot does not start next to BOXl-, since the state:

NEXTTO(ROBOT BOXl) 1Pl2 1P23 IP31

is a member of partitionl . Hence by applying push(BOXl BOX2) we move out of partitionl, and must create a new partition2, specified by:

Partition2: Pl2 1\ 1P23 {\ IP3l.

Similarly , we create partition3

Partition3: 1Pl2 !\ P23 /\ ll'31, and

Partition4: IP12 {\ 1P23 1\ P3l . (see Figure 1.)

From partition2, we can either go to partitionl by doing, for example, push(BOX2 BOX3); or st ay in parti­ tion2 by doing , among other possibilities, goto(BOX2 ); or move to a new

PartitionS : Pl2 1\ P23 1\ IP31,

by applying push(BOX3 BOX2) to the state including : NEXTTO(ROBOT BOX3 ) Pl2 IP23 1P31

of partition2. Similarly , we create:

Partition6: Pl2 IP23 P31, and Partition? : !Pl2 P23 P31 .

At that point, however, no new partitions can be created! Every legal move either leaves the robot in the same partition, or takes her to one of the other partitions. Since the goal state is not in any of the partitions, the disproof is complete. W.W .W.

DISPROVER, programmed in LISP 1.5 and run interpreted on the University of Texas CDC 6600 found the above disproof, for the complete world of [1], in about 7 seconds.

Another disproof, in the world of [1], concerns the goal: AT(BOXl A) STATUS(LIGHTSWITCHl ON), starting from the original state which includes: AT(BOXl A) STATUS(LIGHTSWITCHl OFF). The robot needs to climb on BOXl to turn on LIGHTSWITCHl, but she is then incapable of returning BOXl to its original location. The dis­ proof, by DISPROVER, took about 3 seconds; three partitions were built using the anchor predicates from the goal state.

5.1 Classes of Impossible States.

Given some axiomatization of a world, namely an ini­ tial state and a set of legal moves -operators-, we can distingu ish broadly between two main classes of impossible goal states:

a) goals including a subgoal which is not satisfied in the initial state and does not occur on the add set of any operator. For example, if the robot can­ not paint, and if COLOR(BOXl BLUE) i s true initially, then a goa l including COLOR(BOXl PINK) cannot be achieved, and is di sproved easily by DISPROVER using only one partition.

A variation of this class of impossible tasks occurs when a subgoal, subgoa l., of the goal is satisfied in the initial world but mGst be destroyed, i.e. deleted, to achieve some other subgoa~. Moreover, once de­ leted , ' subgoal. cannot be added by any operator. The last example i~ section 5 above is a case in point. b) Each subgoal. of the goal can be ach ieved indepen­ dently, but the §imultaneous realization of all sub­ goals is impossible, due to "side effects" caused by the delete sets. The main example in section 5 of the symmetric NEXTTO(BOX. BOX.) is a case in point .

1 J

In practice, what is most fun to do is to take someone else's world and disprove goal states which "intui­ tively" should be realizable~

5.2 Selection and Testing of Operators.

Given a set {U} of anchor predicates in an at tempted disproof, DISPROVER first discards al l operators which do not add or delete some predicate in {U}, since these operators are clearly irrelevant. The initial world is intersected with {V} = {PIP-dU} v ,pe:{u}} to gi ve the first partition. All remaining (relevant) oper a­ tors are applied to this partition in an attempt to create new partitions. Whenever a new partition is created, a test is made to see whe ther the goal s tate is in the part ition. If it 'i s , the disproof fails, and DISPROVER will try to bootstrap itself (section 6.) Otherwise, the partition is kept, and all relevant operators will be appl ied to it to try and obtain ye t furthe r new partitions. In artificial intelligence jargon, DISPROVER generates partitions breadth-first until the goal state is found -meaning the disproof failed for the given set of ~nchor predicates (see section 6)- or until no new partitions are found, wh i ch would then complete the disproof.

It should be noticed that with the form of precondi­ tions used, only a few simple set operations are need­ ed to determine whether an operator is applicable to a partition. If preconditions are gene r alized to arbi­ trary predicate calculus expressions, or include pro­ cedures, then it may well be impossible to decide whether an operator is applicable to a partition.

6. Bootstrapping in DISPROVER.

The anchor predicates -which determine the partitions­ are crucial for DISPROVER to be successful. In some cases, DISPROVER can change its set of anchor predi­ cates. We sha ll use a disproof as an example of this capability. We expand the world discussed previously via an operator gotoloc(loc), meaning : robot goes to location loc in room rm.

Preconditions: ONFLOOR ~ 3rm( LOCINROOM(loc rm) ). Delete set: ATROBOT($) NEXTTO(ROBOT $). Add set: ATROBOT(loc).

We will disprove the state ATROBOT(Al), where Al was used in AT(BOXl Al). As in [1], there is no predi­ cate LOCINROOM(Al x) for any x, hence the task i s ob­ viously impossible in the axiomatization .

The initial anchor predicate is obtained from the goal :

ATROBOT(Al).

The initial state is contained in the partition: Partitionl: IATROBOT(Al).

The state : ONFLOOR A LOCINROOM(Al x), for x any thing, is a member of this partitionl -even though it is unat­ tainable-, and the operator go toloc(Al ) can be applied to this state, to obtain

Partition2: ATROBOT(Al).

Since the goal we are trying to disprove is a member of partition2, the disproof fails.

At this point, DISPROVER tries to extend its set of anchor predicates by adding to those already used, all those that were preconditions of the operator(s) that permitted a transi tion t o the partition (here parti­ tion2) which we were hoping not to reach in the dis­ proof. The new set of anchor predicates is: ATROBOT(Al) A ONFLOOR A LOCINROOM(Al x) .

DISPROVER tries again (and wi ll succeed with the dis­ proof, otherwise we would not have chosen this example~) The original state is in:

Partitionl: IATROBOT(Al) " ONFLOOR fl -,LOCINROOM(Al x). From this partition, if the robot climbs on something , we can go to:

Partition2: 1ATROBOT(Al)" ·ONFLOOR fl ILOCINROOM(Al x). However, no further partitions can be generated , com­ pleting the disproof. W.W .W.

DISPROVER finally fai ls to find a disproof if -besides economic reasons of time limit or memory exceeded- no new sets of anchor predicates are gene r ated during boot­ strapp ing.

7. LAWALY helped by DISPROVER.

Up to this point we have seen DISPROVER working alone . Now we will consider cooperation between LAWALY and DISPROVER. In some cases, LAWALY, tge path-finder we use to solve robot planning problems , does not find a path even though one exists. An example will help to illustrate the difficulties she encounters. Figure 2 shows the initial and final s t ates of the robot world. The robot must achieve : CLOSED(DOOR) A NEXTTO(ROBOT BOX), f rom the initial s t ate : INROOM(ROBOT A) "CLOSED (DOOR) A INROOM(BOX B). (See Figure 2.) LAWALY may decide to work first on the CLOSED(DOOR) condition, or f irst on the NEXTTO(ROBOT BOX) condition. Consider the fi rst case. LAWALY finds the door a lready closed in the initial state, so she wan ts to obtain the NEXTTO condition. To do that, she must enter Room B, and to do that go through the DOOR. But that would mean open­ ing the DOOR, and hence undoing what she had already ach ieved, -CLOSED(DOOR)-, and so she decides to try the conditions in the reverse orde r. To be NEXTTO(ROBOT BOX), she goes to DOOR, opens it, goes through it, and then goes next to BOX. At that point, she realizes that she must still close the DOOR. However, that would make her undo some thing she wanted, namely, NEXTTO(ROBOT BOX), so she quits, having failed.

The problem is now passed to DISPROVER. The anchor predicates are taken from the goal, and the followin g partitions are built:

Partitionl: lNEXTTO(ROBOT BOX) CLOSED(DOOR).

Part it ion2: lNEXTTO (ROBOT BOX) lCLOSED(DOOR) .

Partition3: NEXTTO(ROBOT BOX) lCLOSED(DOOR).

Partition4: NEXTTO (ROBOT BOX) CLOSED(DOOR).

Since Partition4 includes our goal, the di sproof fails.

Partition4 was obtained by applying the operator: gonext(object), Preconditions: (ONFLOOR) fl 3x(INROOM (ROBOT x) A INROOM(object x) ), to the state interme­ diary-state: ONFLOOR fl INROOM(ROBOT B) A INROOM(BOX B). DISPROVER suggests to LAWALY that the original problem might be solved by splitting it up into two successive problems. The first problem is to go from the initial s t ate to a state containing intermediary-state above; the second problem is to go from there to the final state. LAWALY does in fact solve the original problem in this way.

8. A Collaborative Failure.

We now describe a solvable task which is not solved by the collaboration between DISPROVER and LAWALY.

The initial and final states of the task are shown in Figure 3 . The final state is: ON(ROBOT BOX) A INROOM (ROBOT B). Again, for essentially the same reasons as before, LAWALY fails to solve the problem. DISPROVER cannot find a disproof (of course, since none exists), but suggests the intermediary-state: INROOM(ROBOT B) ~ NEXTTO(ROBOT BOX). Once more, LAWALY fails, again due to her stubbornness in insisting on finishing a subtask completely before starting another one. DISPROVER finds no disproof (rightly so, since none exists) with the anchor predicates: INROOM(ROBOT BOX) NEXTTO(ROBOT BOX) ON(ROBOT BOX). Moreover, DISPROVER suggests the same intermediary­ state as before, hence the system would begin to re­ peat itself, and failure ~s accepted.

We are investigating the possibility of LAWALY helping DISPROVER by communicating information on why she failed to find a path, thereby helping DISPROVER to build a more adequate set of anchor predicates. The results are st ill sketchy and will not be discussed here.

9. The Importance of Axiomatization.

The problem of section 7 could have been solved imme­ diately by LAWALY, without DISPROVER' s help, if it had

been further spec ified as : CLOSED(DOOR) NEXTTO(ROBOT BOX) INROOM(ROBOT B). The problem of section 8 could have been solved immediately by LAWALY if it had been further specified as : INROOM(ROBOT B) ON(ROBOT BOX) INROOM(BOX B). It could also be solved immediately by LAWALY if the climbon operator had specifi~d as parts of its preconditions that the robot could climb on an object only if both she and the object were in the same room. Thus, we can see that the difficulties encountered may be due to the axiomatization used.

Another way of resolving the difficulties is to "patch" the goal descriptions to include consequences such as: a robot is in the same room as the object she is on, etc. Such a "patch" is a trivial program.

10. Conclusions.

The technique of hereditary partitions permits the disproofs of statements that cannot be made true. We have applied this technique to a disproving program (perhaps the first such program in existence) which operates in simulated robot worlds. DISPROVER can be used to ascertain that physically undesirable states cannot occur in a model. We give examples of collabo­ ration between DISPROVER and a powerful robot planning system, LAWALY. The axiomatization chosen for the world grea tly influences the performance of the des­ cribed systems.

11. References.

1 Fikes, R. E. and Nilsson, N.J . "STRIPS: A New Ap­ proach to the Application of Theorem Proving in Prob­ lem Solving ," Artificial Intelligence, 1, 189-208 , 1971.

2 Review of [1]. Computing Reviews, 1], 5, 216-217, 1972.

3 siklbssy, L. Modelled Exploration by Robot. Techni­ cal Report 1, Computer Sciences Dept., University of Texas, Austin, 1972.

4 simon, H. A. On Reasoning about Actions, in: Simon,

• I H. A. and Siklossy , L. (Eds.) Representation and Meaning: Experiments with Information Processing Sys tems, Prentice-Hall, Englewood Cliffs, N.J., 1972.

5 sikl6ssy , L. and Dreussi, J. A Hierarchy-Drive n Robot Planner which Generates its own Procedures. Technical Report 11, Computer Sciences Dept., University of Texas Austin, 1973.