New Generation Computing, 8 (1990) 225-244 OHMSHA, LTD. and Springer-Verlag

9 OHMSHA, LTD. 1990

A New Deductive Approach to Planning* Steffen H O L L D O B L E R * International Computer Science Institute, 1947 Center Street, Suite 600, Berkeley, CA 94704, USA. Josef SCHNEEBERGER ~ FG Intellektik, FB Informatik, Technische Hochschule Darmstadt, AlexanderstraBe 10, 6100 Darmstadt, Germany (IV) Received 26 October 1989 Revised manuscript received 6 July 1990

Abstract We introduce a new deductive approach to planning which is based on Horn clauses. Plans as well as situations are represented as terms and, thus, are first-class objects. We do neither need frame axioms nor state-literals. The only rule of inference is the SLDE-resolution rule, i.e. SLD-resolution, where the traditional unification algorithm has been replaced by an E-unification procedure. We exemplify the properties of our method such as forward and backward reasoning, plan checking, and the integration of general theories. Finally, we present the calculus and show that it is sound and complete. Keywords: Logic Programming, Deductive Planning, Equational Reasoning.

w

Introduction

In the last,30 y e a r s o f research in A I p l a n n i n g there have a l w a y s been two m a i n d i r e c t i o n s . T h e first a n d m o r e f a v o r i t e one aims at b u i l d i n g efficient a n d i n t e l l i g e n t systems w h i c h generate p l a n s for c o m p l i c a t e d d o m a i n s . T h e s e c o n d a p p r o a c h tries to use results a n d m e t h o d s f r o m a u t o m a t e d t h e o r e m p r o v i n g , to s h o w the usefulness o f these m e t h o d s , a n d to b u i l d p l a n n i n g systems w i t h a well defined semantics. A l t h o u g h these " d e d u c t i v e " systems are n o t a b l e to c o p e w i t h the h a r d p r o b l e m s solved b y the " k n o w l e d g e - b a s e d " systems, the results w h i c h *

An earlier version of this paper was presented at the German Workshop on Artificial Intelligence, 1989. On leave from FG lntellektik, Technische Hochschule Darmstadt. This work was partly funded by a grant from Siemens AG, M13nchen.

226

S. H~lldobler, and J. Schneeberger

are produced in this area are often very useful to understand what planning systems really do and how their capabilities can be improved. Most (but not all) deductive planners are still linear planners, i.e. the plans which they handle and produce are strictly ordered in contrast to partially ordered nonlinear plans. It is commonly accepted, that a clear understanding of linear planning is a necessary precondition for understanding nonlinear planning. For this reason predicate logic (and also modal logic) is widely used as a specification language to examine new planning principles or to reconstruct old methods. 1'2m On the other hand logic calculi are regarded too inefficient to implement (logic) programs for plan generation, though this has not been proved. Therefore, besides our interest in the semantics of planning systems, our main goal is to apply the elaborate and often very efficient methods developed in automated theorem proving to plan generation. The ideas presented within this paper are in the tradition of approaches like C. Green's system based on QA4. 4) He tried to apply the resolution* principle to planning and also to program synthesis. The main problem which arises with this approach is the need of many frame axioms to solve (or not to solve) the frame problem (identified by McCarthy and HayesS)). R. Kowalski 6~ introduced a different representation of the problem domain (using the meta-predicate H O L D S ) to reduce the number of frame axioms dramatically. But there remains the problem, that deduction has to be guided: The application of the frame axioms must be deferred as long as they are not really necessary for the solution of the problem. Otherwise, the system would produce infinitely many correct but unnecessary theorems about the problem. W. Bibel 7~ also improves the representation of the problem by introducing a single state literal in the preconditions and postconditions of an operator. To handle such operators he uses a modified version of his connection calculus. Thus he is able to avoid frame axioms completely, but the semantics of the resulting calculus had to be redefined (the problems were described by Fronh6ferS~). Three possible solutions based e.g. on modal logic are presen~d by Bibel et al. 9~ This paper introduces an approach which is based on Horn clauses. Plans as well as situations are represented as terms and, thus, are first-class objects. We do neither need frame axioms nor state literals. The only rule of inference is the SLDE-resolution rule, i.e. SLD-resolution, where the traditional unification algorithm has been replaced by an E-unification procedure. In Section 2 we give a brief overview of our approach by solving a simple blocksworld problem. Further properties of our method such as forward and backward reasoning, plan checking, and the integration of general theories are demonstrated in Section 3 using more difficult examples. Section 4 provides the description of the calculus *

C. Green used paramodulation within resolution to achieve equality reasoning.

227

A New Deductive Approach to Planning

and Section 5 discusses the virtues of our solution and points out future work.

w

A Simple Bloeksworld Example

In this section, we depict our basic principle within a very simple example of the well-known blocksworld domain. A certain situation in the blocksworld is specified by a collection of fluents*, 5) about the world. F o r example, the term c(A) o o(A, B ) o t ( B ) o e denotes the situation (in Fig. 1), where the block A has a clear top and sits on block B; block B itself is located on the table and the hand of the robot is empty. A plan is a sequence of actions, which when executed transforms one situation into another. F o r example, executing the plan unstaek (A, B): putdown (A) transforms the situation given above into the situation t(A) o t ( B ) o c(A) o c ( B ) o e as shown in Fig. 1 by lifting A from B and putting it on the table.

I

I

I

I

I

I

Fig. 1 The most simple bloeksworld example.

In this example and throughout this paper, we use A, B, C .... as constants and p, u, v, w .... as variables. Formally, a situation is now represented by either r or x o y, where o is a binary function symbol written infix and x, y are fluents respectively situations. We assume that o is associative, commutative, and r is its identity. Plans are represented by either A or p~ : p2, where A denotes the empty plan, : is a binary function symbol written infix, pl is a plan, and p2 is a single operation. For notational convenience we omit A and parenthesis when writing plans by assuming that they are associated to the right. In the sequel let E be the equational theory which specifies the fact that o is associative, commutative, and r the identity of o, i.e. E consists of the axioms x o (y o z) = (x o y ) o z x o y = y o x x o r = x.

(A) (C) (l)

We denote the fact that the execution of a plan p transforms situation s into situation r by the atom P L A N ( s , p, r). s and r are called the current (or initial) and goal situation, respectively. Conventional approaches such as Green's QA4 4) do not distinguish between object and meta level: the fact that a certain fluent holds is represented *

Fluents are predicates which are (not) valid in a certain situation. Fluents can also be stated as functions over situations.

S. H611dobler, and J. Schneeberger

228

as an atom. Kowalski 6~ did use a meta-predicate to represent fluents, but in our approach (complete and partial) situations as well as plans are represented as terms and, thus, are first-class objects. We reason about worlds and plans and it turns out that we can omit the use of frame axioms entirely. As a consequence, the "STRIPS assumption ''1~ has to hold for our operator definitions. For example an action like the blocksworld putdown-operator is formalized as the (universally closed) Horn clause P L A N ( x , p : p u t d o w n ( v ) , z o t ( v ) o c(v) o e) r P L A N ( x , p, z o h ( v ) ) ,

(D)

where h ( v ) denotes that the robot holds block v. The operator is read declaratively as the execution of the plan p : p u t d o w n ( v ) transforms situation x into situation z o t ( v ) o c(v) o e if the execution o f p transforms x into z o h ( v ) or procedurally as to solve the problem of whether there exists a plan p : p u t d o w n ( v ) such that its execution transforms the situation x into situation z o t ( v ) o c(v) o e solve the problem of whether there exists a plan p such that its execution transforms situation x into situation z o h(v). Now, the unstaek-operator can be defined as P L A N ( x , p : u n s t a c k ( v , w), z o h ( v ) o c ( w ) ) r P L A N ( x , p, z o c(v) o o(v, w) o e).

(U)

Observe, we have nothing to plan if the goal situation is contained in the current situation. However, we have to ensure, that the current as well as the goal situation are consistent. This is specified by the termination rule PLAN(x

o y , A, x ) r

CONSISTENT(x) /X C O N S I S T E N T ( x

o y)

(T)

which tells us, that a goal could be reached without an action, if it is already part of the current situation. It ,is not sufficient to guarantee consistency of the complete situation, viz. x o y only, because it may still contain an inconsistent partial situation. As an example, consider our blocksworld to include balls (termed b a l l ( x ) ) and cups (termed c u p ( x ) ) and the consistency constraint that balls may only sit on top of cups. Hence, the situation o ( A , B ) o t ( B ) o c ( A ) o e o b a l l ( A ) o c u p ( B ) is consistent while its part o ( A , B ) o t ( B ) o c ( A ) o e o b a l l ( A ) is not. Consistency has to be specified in terms of the problem domain. For example, it cannot be the case that in a certain situation block A is located on

A New Deductive Approach to Planning

229

block B and on the table. Obviously, the consistency can be specified by a possibly infinite set o f clauses o f the form

C O N S I S T E N T ( t( A ) ) r C O N S I S T E N T ( t ( A ) o e) r C O N S I S T E N T ( t ( A ) o c(A)) r However, if we assume that a certain situation is consistent if and only if it is not inconsistent, then we can use the clauses

CONSISTENT(x) r NOT(INCONSISTENT(x)) INCONSISTENT(x o x o y)r INCONSISTENT(h(v) o e o x) r I N C O N S I S T E N T ( h( v) o o(w, v) o x ) r I N C O N S I S T E N T ( h( v) o o(v, w) o x ) r I N C O N S I S T E N T ( h( v) o c(v) o x ) r I N C O N S I S T E N T ( c( v) o o(w, v) o x)r I N C O N S I S T E N T ( t ( v ) o o(v, w) o x ) r I N C O N S I S T E N T ( t ( v ) o h(v) o x ) r I N C O N S I S T E N T ( h( v) o h(w) o x) C=v4= w I N C O N S I S T E N T ( o( u, v) o o( w, v) o x) r u 4= w I N C O N S I S T E N T ( o ( u, v) o o(u, w) o x)<== v :r w

(IC) (I1) (I2) (13) (14) (15) (16) (17) (I8) (19) (I10) (Ill)

together with the negation-by failure rule. ") Clause (I1) expresses a minimality condition in the sense that the fact that a certain fluent holds is stated at most once. (19), on the other hand, states that the robot arm cannot hold two different blocks at the same time. If, on the other hand, v and w in (19) where identical, clause (I1) w o u l d again reduce the situation. As we will see in Section 4, the consistency constraints o f the termination rule are sufficient to ensure that only those plans are generated, which transform consistent initial situations into consistent goal situations. One should observe, that there is no need to wait with the consistency check until the termination rule is applied. We could as well check the consistency o f the current and goal situation o f an initial query posed to our planning program or somewhere in the middle o f a deductioh. The consistency has to be checked only once and the design o f the various actions guarantees that the situations are still consistent after an action has been performed. Of course, this has to be proved (see Theorem 4.2). C o m i n g back to our example o f Fig. 1 we can n o w ask the question of whether there exists a plan p such that its execution transforms situation c ( A ) o o ( A , B ) o t ( B ) o e into t ( A ) o t ( B ) o c ( A ) o c ( B ) o e. More formally, we pose the query

S. H~511dobler, and J. Schneeberger

230

r

P L A N ( e c) c(A) o o(A, B ) o t(B), p, e o c(A) o c ( B ) o t(A) o t(B))

to our program consisting of the clauses (D), (U), (T), and the Consistency axioms. To answer this question we have to show that there exists a binding r for such p that P L A N ( e o c(A) o o(A, B ) o t(B), r, e o c(A) o c ( B ) o t(A) o t(B)) is a logical consequence of our program under the equational theory E mentioned earlier. This can be done by using SLDE-resolution, xz'13) i.e. SLDresolution, where the traditional unification algorithm has been replaced by a complete E-unification procedure. In our case, we need an A Cl-unification procedureJ 4) A p p l y i n g SLDE-resolution to our initial goal clause using a new variant of (D) (variables are indexed) and the substitution { x l / e o c ( A ) o o(A, B ) o t(B), P/I~ : putdown(A), zff c ( B ) o t(B),

vl/ A } we obtain r

P L A N ( e o c(A) o o(A, B ) o t(B), pl, h(A) o c ( B ) o t(B)).

Applying SLDE-resolution again using a new variant of (U) and {x2/e o c ( A ) o o(A, B ) o t(B), pl/p2: unstack(A, B), zz/t(B), v2/

results in r

P L A N ( e o c(A) o o(A, B ) o t(B), 1)2, c(A) o o(A, B ) o e o t(B)).

To this goal we apply our termination rule with the substitution {xa/e o c(A) o o(A, B ) o t(B), p2/A, ya/qJ} and obtain the goal clause r

C O N S I S T E N T ( e o o(A, B ) o t(B) o c(A))A C O N S I S T E N T ( e o o(A, B ) o t ( B ) o c(A)).

Since e o o(A, B ) o t ( B ) o c(A) is consistent we can derive the empty clause D. Composing the substitutions used in the refutation and restricting it to the variable p we obatin the computed a n s w e r substitutlon { p / u n s t a c k ( A , B ) : putdown(A)}. In other words, we have generated the plan unstack(A, B ) : p u t d o w n ( A ) by b a c k w a r d reasoning.

A New Deductive Approach to Planning

231

One should observe, that in contrast to Kowalski 6) we do not have to specify that certain facts do not hold anymore after an operation has been performed. To clarify this point, let us again have a l o o k at the first SLDEresolution step o f the previous refutation. To be able to apply SLDE-resolution to the initial goal clause we had to solve the problem o f whether e o c(A) o c(B) o t(A) o t(B) and zl

o

t(Vl)

o

C(Vl) 0 e

are unifiable under the equational theory which specifies that o is associative, commutative, and ~b is its identity. This unification problem has the two most general solutions {vl/A, zl/e(B)

o

t(B)}

and {valB, z l / e ( A ) o t(A)}. In the previous refutation we have chosen the first solution. Note, the terms e(A), t(A), and e were "consumed" by the need to unify with the terms C(Vl), t(Va), and e, whereas Zl was instantiated with the remaining fluents, that did not occur in the postconditions of the putdown-operator. In other words, z~ was bound to the part of the situation, which remained unchanged. As a consequence, if we define an operator such as P L A N ( x , p : putred(v), z o t(v) o c(v) o e o red(v)) r P L A N ( x , p, z o h(v) o red(v)), which puts down only red blocks, we have to state that the block is still red after the putred operator has been applied. But note, this is only necessary for fluents which are required as preconditions, but are not "consumed" by the operator. In general, the variables x and z used in the clauses for the operators play the role of state-variables in the situation calculus. 5) In our a p p r o a c h we do not need a state literal, which is used, to record - - a s a side-effect'---the generated plan. 7) We represent both situations and plans by terms, we reason about situations and plans on the object level and a generated plan corresponds precisely to the well-known concept of a computed answer substitution in logic p r o g r a m m i n g languages) s) We will come back to this point in Section 4.

w

More Examples

In this section we give more examples to illustrate our approach. We particularly show how in the blocksworld operators can be applied forward as well as backward, how the contents of two registers can be swapped, and how

S. HSlldobler, and J. Schneeberger

232

a pair of socks having the same colour can be found in a dark room.

3.1

The Blocksworld So far we have defined only the two operators unstack and putdown, which are necessary to solve the planning problem depicted in Fig. 1. Let us now give the list o f our blocksworld operators. (1]

The operators The following specification o f the well-known blocksworld robot operations shows always a "backward" operator. That means, the search is directed by the postconditions of the operators and the goal situation. Pickup (P)

P L A N ( x , p : pickup(v), z o h(v)) r P L A N ( x , p, z o c(v) o t(v) o e)

Unstaek P L A N ( x , p : unstack(v, w), z o h(v) o c ( w ) ) r P L A N ( x , p, z o c(v) o o(v, w) o e)

(U)

Putdown (D)

P L A N ( x , p : p u t d o w n ( v ) , z o t(v) o c(v) o e) r P L A N ( x , p, z o h ( v ) )

Stack (S)

P L A N ( x , p : stack(v, w), z o o(v, w) o c ( v ) o e) r P L A N ( x , p, z o c ( w ) o h(v))

Termination PLAN(x r

o y, A, x ) CONSISTENT(x)

(T) A CONSISTENT(x

(2)

o y)

Sussman's "Anomaly" Using SLDE-resolution and the clauses defined in the previous section we can solve Sussman's "Anomaly". 16~ It should be noted that Sussman's "Anomaly" is only a hard problem in an incompletely specified problem domain, whereas our approach handles only completely specified goals. For humans it's fairly obvious how a plan must look like, that solves Sussman's " A n o m a l y " , namely

I

I

I

i

I

i

Fig. 2 A blocksworld example (the Sussman "Anomaly").

A New Deductive Approach to Planning

233

unstack( C, A) : putdown( C) : pickup(B) : stack(B, C) : piekup(A) stack(A, B).

That this is indeed a correct plan can be verified by posing the query e= P L A N ( e o c ( C ) o c(B) o o(C, A) o t(B) o t(A), unstack( C, A) : putdown( C) :pickup(B) : stack(B, C) pickup(A) : stack(A, B), e o c(A) o o(A, B ) o o(B, C) o t ( C ) )

to our blocksworld program which consists of the clauses (P), (U), (D), (S), (T), and the clauses for checking the consistency of situations. The interested reader may verify that we obtain the following SLDE-refutation by using the clauses (S), (P), (S), (P), (D), (U), (T), and Consistency clauses in this sequence: e= P L A N ( e o c( C) o c(B) o o( C, A ) o t(B) o t(A), unstack( C, A) : putdown( C) : pickup(B) : stack(B, C) : pickup(A), c(B) o h(A) o o(B, C) o t( C)) e= P L A N ( e o c ( C ) o c(B) o o(C, A) o t ( B ) o t(A), unstack( C, A) : putdown( C) :pickup(B) : stack(B, C), c(B) o c(A) o t(A) o e o o(B, C ) o t ( C ) ) r P L A N ( e o c ( C ) o e(B) o o(C, A) o t(B) o t(A), unstack( C, A) : putdown( C) :pickup(B), c(A) o t(A) o e ( C ) o h ( B ) o t ( C ) ) e= P L A N ( e o c ( C ) o c(B) o o(C, A) o t(B) Q t(A), unstack( C, A) : putdown( C ), c(A) o t(A) o e ( C ) o e(B) o t(B) o e o t ( C ) ) r P L A N ( e o c ( C ) o c(B) o o(C, A) o t(B) o t(A), unstack( C, A), e(A) o t(A) o c ( B ) o t(B) o h ( C ) ) e= P L A N ( e o c ( C ) o c(B) o o(C, A) o t(B) o t(A), A, t(A) o c(B) o t ( B ) o c( C) o o( C, A) o e) e= C O N S I S T E N T ( e o c ( C ) o c(B) o o(C, A) o t ( B ) o t(A)) A' C O N S I S T E N T ( e o c(C) o c(B) o o(C, A ) o t(B) o t()l)) , . .

D.

From the completeness of SLDE-resolution (see Theorem 4.3 in Section 4) we learn that for each correct plan there exists an eventually more general computed plan. In other words, the above mentioned plan can also be generated by SLDE-resolution. In the case of generating a plan, the necessity to guide search becomes obvious. However, the issue of control is outside the scope of this paper.

S. H611dobler, and J. Schneeberger

234

(3)

Forward planning

So far we have applied our blocksworld operators backwards. If we want to direct the search by the preconditions of the operators and by the current situation, then we can use the program clauses P L A N ( c ( v ) o t(v) o e o x, pickup(v) :p, z) r P L A N ( h ( v ) o x, p, z) P L A N ( c ( v ) o o(v, w) o e o x, unstack(v, w) : p, z) <==P L A N ( h ( v ) o c(w) o x, p, z) P L A N ( h ( v ) o x, putdown(v) : p, z) r P L A N ( c ( v ) o t(v) o e o x, p, z) P L A N ( c ( w ) o h(v) o x, stack(v, w): p, z) <==P L A N ( o ( v , w) o c(v) o e o x, p, z) P L A N ( x o y, A, x ) r C O N S I S T E N T ( x ) A C O N S I S T E N T ( x o y)

(P') (U') (D') (S') (T')

together with the clauses to check the consistency of situations and we will achieve the same results. (We also have to change our representation of plans as follows: A denotes the empty plan and p~ : pz denotes the operator/h followed by the plan/~. Again we omit A and parenthesis by assuming that plans are associated to the left.) To exemplify this we solve Sussman's "Anomaly" by applying SLDE-resolution using the clauses (U'), (D'), (P'), (S'), (P'), (S'), (T'), and the Consistency clauses to r

P L A N ( e o c( C) o e ( B ) o o( C, A) o t ( B ) o t(A), P, e o c(A) o o(A, B ) o o(B, C ) o t ( C ) )

to obtain the following SLDE-refutation r

r

r

r

r

P L A N ( h ( C ) o c(A) o c ( B ) o t ( B ) o t(A), P~, e o c(A) o o(A, B ) o o(B, C) o t ( C ) ) P L A N ( c ( C) o t( C) o e o e ( A ) o c(B) o t ( B ) o t(A), p2, e o c(A) o o(A, B ) o o(B, C) o t ( C ) ) P L A N ( c ( C ) o t ( C ) o c(A) o t(A) o h ( B ) , t~, e o c(A) o o(A, B ) o o(B, C) o t ( C ) ) P L A N ( t ( C ) o c(A) o t ( A ) o o(B, C ) o c ( B ) o e, p4, e o e(A) o o(A, B ) o o(B, C) o t ( C ) ) P L A N ( t ( C ) o o(B, C) o c ( B ) o h(A), 1~, e o c(A) o o(A, B ) o o(B, C) o t ( C ) )

A New Deductive Approach to Planning

235

r P L A N ( t ( C ) o o(B, C) o o(A, B) o c(A) o e, p6, e o c(A) o o(A, B) o o(B, C) o t ( C ) ) r C O N S I S T E N T ( e o c(A) o o(A, B) o o(B, C) o t( C)) A C O N S I S T E N T ( e o c(A) o o(A, B) o o(B, C) o t(C))

where p is successively instantiated to

unstack( unstack( unstack( unstack( unstack(

- ,,

C, C, C, C, C,

A):/~

A) A) A) A)

: putdown( C) : t~ : putdown( C) : pickup(B) :1)3 : putdown( C) : pickup(B) :stack(B, : putdown( C) : pickup(B) :stack(B, pickup(A) :1~ unstaek( C, A) : putdown( C) :pickup(B): stack(B, pickup(A) : stack(A, B) : t~ unstack ( C, A) : putdown( C) :pickup(B) :stack(B, pickup(A) : stack(A, B) : A.

C) : p4 C): C) : C) :

We may also combine forward and backward reasoning by taking clauses from {(P), (U), (D), (S), (T)} and {(P'), (U'), (D'), (S')} as input clauses.

3.2

Register Transfer

The task of the register transfer problem in Fig. 3 is to exchange the contents (A and B ) o f two registers I and J o f some computer with the help o f a third register K which serves as a buffer. We define a new operator transfer by

P L A N ( w , p: transfer(x, y), z o c(x, v) o c(y, v)) r P L A N ( w , p, z o c(x, v) o c(y, u))

(TR)

where the term c(x, v) states that register x has content v. We also need our old termination rule (T). Observe, that u, v.... are variables. Thus, in Fig. 3 we have stated that we d o not care about the contents of register K in the current as well as in the goal situation. In the register-transfer example a situation is consistent if each register is mentioned at most once, which can be expressed by

Register I := A Register J := B Register K := u

Register I := B Register J := A Register K := v

Fig. 3 The register transfer example.

236

s. H5lldobler, and J. Schneeberger

CONSISTENT(c(i, x)) r CONSISTENT(c(j, x)) r CONSISTENT ( c( k, x ) ) r CONSISTENT(e(i, x) o c(j, y)) r CONSISTENT(r x) o e(k, y)) r CONSISTENT(e(j, x) o e(k, y)) r CONSISTENT(c(i, x) o r y) o e(k, z)) r or, if we assume that our world is closed m by

CONSISTENT(w) r NOT(INCONSISTENT(w)) INCONSISTENT(c(x, y) o e(x, z) o w) r Our problem can now be stated as

<==P L A N ( e ( I , A) o c(J, B) o e(K, u), p, e(I, B) o e(J, A) o e(K, v)). To solve this goal we apply SLDE-resolution using a new variant o f (TR) and the substitution

{wt/e(l, A) o e(J, B) o e(K, u), p/p~ : transfer(K, I), z~/c(J, A), x~/K, )11/1, v~/B, v/B} to obtain

r PLAN(e(I, A) o e(J, B) o e(K, u), pl, e(J, A) o e(K, B) o e(I, ul)). Similarly, using again (TR) and the substitution

{ wJe(I, A) o e(J, B) o e(K, u), pl/pz : transfer(I, J), z J c ( K , B), xz/I, y2/J, v2/a, u~/A} results in

r P L A N ( c ( I , A) o c(J, B) o e(K, u), pz, c(K, B) o c(I, A) o e(J, uz)). Using (TR) again and the substitution

{ w3/c(l, A) o c(J, B) o c(K, u), pz/p3 : transfer(J, K), z J c ( I , A), x3/J, y J K , vJB, uz/B} yields

r PLAN(c(I, A) o c(J, B) o e(K, u), 1~, c(I, A) o c(J, B) o c(K, ua)). Finally, we apply SLDE-resolution using our termination rule and the substitution

A New Deductive Approach to Planning

237

{x4/c(I, A) o c(J, B) o c(K, u), y4/r p J A , u J u } and obtain

r

C O N S I S T E N T ( e ( I , A) o e(J, B) o c(K, U)) A C O N S I S T E N T ( e ( I , A) o c(J, B) o c(K, U)).

The empty clause can easily be derived by using C O N S I S T E N T clauses and we obtain the computed answer substitution

{v/B, p/transfer(J, K) : transfer(I, J) : transfer(K, I)}. If we restrict this substitution to p, we find the generated plan, which solves the register-transfer problem. 3.3

3-Socks Problem Our next example shows that we may include general theories within our approach. The problem is to pick a pair of socks of the same colour out of a drawer in a dark room. The drawer contains a lot of socks (more than four) half of them are white and half black. We use a term h(x, y) to state that we hold x socks of one colour and y socks of the other colour in our hand. But now we have to count the number of socks in our hand. Therefore, we will use the following axioms for the addition of natural numbers O+y

=y

(+1) (+2)

s(x) + y ---- s(x + y),

where 0 denotes the natural number zero and s denotes the successor function on natural numbers. Let us adopt the notational convention that a number sn(0) is abbreviated by n. We also have to express that a certain number x is greater (resp. greater or equal) than a number y. To keep our example small, we will use the equation x = s(y) + z (resp. x = y + z) to express this fact. In general, however, we can define any conditional equational theory. Since in this example a situation is completely defined by a term of the form h(x, y) we do not need the equational theory E as in the blocksworld or register-transfer example. Instead we will use an E-unification procedure for ( + 1 ) and ( + 2 ) . Our operators in this example can now be defind as

P L A N ( u , p : takeone, r PLAN(u, P L A N ( u , p : takeone, r PLAN(u,

h(s(x), y)) p, h(x, y)) A x = y h(x, s(y))) p, h(x, y)) A x = s(y) + z.

(T1) (T2)

(T1) states that we will pick up an additional sock of one colour if we perform the operation takeone in a situation where we have equally many socks of both colours. (T2), on the contrary, states that we might pick a sock of the wrong

238

s. HSlldobler, and J. Schneeberger

colour if we already have more socks of one colour (x) than of the other (y). This is a somewhat pessimistic statement but we want to take enough socks to have at least one complete pair of socks. Because equations like x = s(y) + z may occur as subgoals in a goal clause we also need the axiom x = x <:=

(R)

of reflexivity. Furthermore, due to the special form of situations in this example we can simplify our termination rule to

P L A N ( u , A, u).

(TS)

The problem to get one pair o f socks o f the same colour starting with no socks in hand can now be stated as

r PLAN(h(O, 0), p, h(2, v)) A 2 = s(v) + w where 2 = s(v) + w is usually written as 2 > v. Since PLAN(h(O, 0 ) , p , h(2, v)) and the head PLAN(u1, p~: takeone, h(s(x~), yx)) of a new instance o f (T1) are unifiable under E = { ( + 1), ( + 2 ) } with substitution {ul/h(O, 0), p/pl : takeone, xl/1, yx/v} we can derive

<:=PLAN(h(O, 0), pl, h(1, v)) A 2 = s(v) + w A 1 = v by SLDE-resolution. The equations in this goal clause can be solved by using the axiom of reflexivity twice with the substitutions { v/1 } and { w/0}, respectively. Thus, we obtain

r PLAN(h(O, 0), px, h(1, 1)), to which SLDE-resolution can be applied using a new variant of (T2) and substitution

{u2/h(O, 0), pl/p~ : takeone, xz/1, y2/0} and resulting in

r PLAN(h(O, 0), p2, h(1, 0)) A 1 = 1 + zz. The equation 1 : 1 + z2 can be solved by binding zz to 0. An additional SLDE-resolution step using (T1) and

{ u3/h(O, 0), Pz/l~: takeone, x3/0, y3/0} yields

r PLAN(h(O, 0), p3, h(O, 0)) A 0 = O. Now, the empty clause can easily be derived in two additional SLDE-resolution

A New Deductive Approach to Planning

239

steps using (R) and (TS) and we obtain the computed answer substitution

{p/takeone : takeone : takeone}. In other words, if we have taken three socks out of the drawer, at least two of them must have the same colour.

w

The Calculus

In this section we formally develop our plan calculus and show that it is sound and complete. We assume readers to be familiar with basic notions and results from logic programming and unification theory as can be found for example in Lloyd 15) and SiekmannJ 4) Recall, each presented example consists of an equational theory E and the set L P of clauses for expressing the various actions and the (In-) Consistency check. Obviously, L P is a Horn clause logic program, or logic program for short, and E is a conditional equational theory. For example, in the blocksworld LP consists of the clauses (P, U, D, S, T ) and the Consistency-Axioms and E consists o f the clauses (A, C, 1), if we want to plan backwards. Since we intend to 0se this example throughout this section we denote this program by (AC1, LPb). But note, all results except Theorem 4.2 hold for each example in this paper. From Jaffar et al. ~8'~9)we know that the main semantic properties of logic programs hold also if a logic programs is augmented with a conditional equational theory. In particular, the semantics of such an equational logic program (E, L P ) can be given as the least Herbrand E-model for LP, M~(LP). ME(LP) is defined over the so-called Herbrand E-universe, which is the quotient of the Herbrand universe modulo the finest congruence relation on ground terms generated by E. For example,

PLAN(Ec(A) o o(A, B) o t(B) o el, Eunstack(A, B) : putdown(A)], It(A) o t(B) o c(A) o c(B) o el) is an element of the least Herbrand E-model of (A C 1, LPb), where Er] denotes the congruence class defined by A C 1 and containing the term r. For notational convenience we abbreviate an atom Q(Erl~, ..., ~rn]) by [Q(rl ..... rn)~. It should be observed, that Is~ = ~r~ if and only if s and r are equal under E.

Theorem 4.1 (Jaffar et al. TM) Let (E, L P ) be an equational logic program and A be a ground atom.

Me(LP) = { [A~IA is a logical E-consequence of LP}. In other words, ME(LP) contains all atoms of the form [PLAN(s, p, r)~, such that the execution of plan p transforms situation s into situation r. The least Herbrand E-model of an equational logic program (E, L P ) can also be

240

S. HNldobler, and J. Schneeberger

characterized by the least fixpoint of the function

T~,L~(I) = { [A]I

there is a ground instance B r B1 A ... A Bn of a clause in L P such that [A] = [B] and {[B1], ..., [Bn]} c_ I},

which maps interpretations onto interpretations. .8) Let T~,Lp ~ 0 = TE,Le(r and TE,Lp ~ (n q- 1) = Tg,I.p(TE,t.p ~ n). As we mentioned in the previous section it suffices to check the consistency of situations after the termination rule has been applied. Of course, we have to show that the application of an operator to a consistent situation yields again a consistent situation. This, however, depends on the various actions of our planning p r o b l e m and has to be proven for each program separately. The following theorem states, that the least H e r b r a n d A C 1-model of LPb contains only consistent situations. T h e o r e m 4.2 (Consistency of ) I f [ P L A N (s, p, t)] ~ MAcl(LPb) then s and t are consistent. Proof We prove by induction on n that if [ P L A N (s, p, r)] ~ TAC~,Lpo ~ n then s and r are consistent. The result follows immediately from the fact that the least fixpoint of TAc~,Lp~ and MAcl(LPb) are identical. Observe, if s is consistent and Is] = [r], then r is also consistent. N o w we will prove our claim. The case n = 0 being trivial we turn to the induction step and assume the result holds for n. Let [ P L A N ( s ' , p', r')] E Tacl.Le~ ? (n + 1). We distinguish two cases with respect to the program clause used in the last application of Tac~,LPo: I f a ground instance of the termination rule (T) has been used, then, obviously, s' resp. r' are consistent. Otherwise, a clause from {(D), (P), (S), (U)} has been used. First, suppose that the ground instance P L A N ( s , p : putdown(A), r o t(A) o c(A) o e) r P L A N ( s , p, r o h(A)) of (D) has been used. By the induction hypothesis, s, r o h(A), and r are consistent. Since Is'] = Is] and [r'] = [r o t ( A ) o c(A) o e] we find that s" is consistent and it remains to show that r o t(A) o c(A) o e is consistent. By contradiction we assume that r o t(A) o c(A) o e is inconsistent and distinguish the following cases (recall, r is consistent by the induction hypothesis): I f t(A) (resp. c(v) or e) occurs in r, then r o h ( A ) would be inconsistent by (I8) (resp. (15) or (12)). If h ( B ) (resp. h ( A ) ) occurs in r, then r o h ( A ) would be inconsistent by (I9) (resp. (I1)).

A New Deductive Approach to Planning

241

If o(B, A) occurs in r, then r o h(A) would be inconsistent by (I3). Finally, if o(A, B) occurs in r, then r o h(A) would be inconsistent by (I4). The cases where a ground instance of (P), (S), or (U) has been used follow analogously. qed We can now turn to the question o f how queries posed to our planning program can be answered. In other words, given an initial and a goal situation, how can we generate a plan whose execution transforms the initial into the goal situation? We intend to use SLDE-resolution as the only inference rule in our calculus. Therefore, we assume to have a sound and complete E-unification procedure build into the SLDE-resolution rule. The following theorem can be found in H611dobler13):

Theorem 4.3 (Soundness and Strong Completeness for SLDE-resolution) Let R be a c o m p u t a t i o n rule and G be a goal clause, and be an equational logic program. EaCh computed answer substitution for LP U { G} wrt SLDE-resolution is a correct answer substitution. For each correct answer substitution d for LP and G, there exists an Rcomputed answer substitution 0 obtained by an SLDE-refutation of LP U { G} such that d is equal or less general under E than 0. A similar but weaker result has been proved by Gallier and Raatz. ~z) They show Theorem 4.3 only for unconditional equational theories and do not prove the independence of the selection function. N o w let p be a correct plan for transforming situation s into situation r by applying the operations from LP iff EPLAN(s, p, r)] ~ Me(LP). Furthermore, let p be a generated (or computed) plan for transforming situation s into r by applying the operations from LP iff x / p is a binding in the computed answer substitution of an SLDE-refutation of LP U {r PLAN(s, x, r)}. The following corollary is an immediate consequence of the previous theorem.

Corollary 4.4 Each generated lblan is a correct plan. For each correct plan p there exists a generated plan, which is equal or more general under E than p.

w

Conclusion

We have presented a new deductive solution to the AI planning problem. Instead of using full first-order logic with equality 4'7) we have restricted ourselves to H o r n clause logic with equality. This bears several advantages. We have a least model and fixpoint semantics and we may use SLDE-resolution to generate plans. Furthermore, the well-known concepts of a correct and computed answer

242

S. HSlldobler, and J. Schneeberger

substitution ~) gives us a declarative reading of a correct and generated plan, respectively. We expect, that our calculus can be efficiently implemented using techniques from logic programming, such as the WAM, TM incorporating special theory unification procedures. TM Since our PLAN-predicate utilizes an explicit representation of the (partially developed) plan, reasoning about plans is possible. This property is shown in the simple case of verifying a given plan, but this could also be used to reorder a sequence o f operators which was planned so far. In the same way we can also handle problems with hierarchically defined operators, because hierarchical planning is only a matter o f problem definition? 2) Obviously, A Cl-unification may not only be used to represent world states as in our example. Analogously, it can be used to represent sets (including multiple copies of elements) in general. For example the predicate M E M B E R can be represented as M E M B E R ( x , x o y).

R. Kowalski zaa4) discusses the advantages of different representations o f this sort o f data structures. We belief, that our approach will lead to very elegant and comprehensive logic programs. However, there are still open problems concerning the computational properties of A C 1-unification. Much work remains to be done. We believe that our approach can be extended to nonlinear planning and incompletely specified problem domains as well. Especially, we would like to investigate how concurrent planning is related to the various forms o f parallelism inherent in (Horn) logic programming languages. Another question is how negative fluents can be handled within our framework. Results presented in a recent paper by Buntine and BfirckertTM point towards a possible solution: Instead of solving only equations under a certain equational t h e o r y - - i n our case A C l - - w e could also solve disequations under the equational theory. Eventually, this leads to a reduced search space, as the examples given by Buntine and Bfirckert suggest.

Acknowledgements This work emerged "from the lively discussions within the Intellektik group at the THD. Special thanks to Elmar Eder, who has identified a bug in an earlier version o f our paper and to Bertram Fronh6fer for his detailed comments on both, the contents and the English style. We are grateful to Wolfgang Bibel for his collection of planning examples, which guided our work in Section 3. Also, we thank our referees for comments that resulted in a number of improvements.

A New Deductive Approach to Planning

243

g eferellge$ 1) Lifschitz, V., "On the Semantics of STRIPS," in Proceedings of the Workshop on Reasoning about Actions and Plans (M. P. Georgeff, and A. L. Lansky, eds.), Morgan Kaufmann Publishers, Los Altos, pp. 1-8, 1986. 2) Chapman, D., "Planning for Conjunctive Goals," Artificial Intelligence, Vol. 32, No. 3, pp. 333-377, 1987. 3) Hertzberg, J. and Horz, A., "Towards a theory of conflict detection and resolution in nonlinear plans," in International Joint Conference on Artificial Intelligence, 1989. 4) Green, C., "Application of theorem proving to problem solving," in International Joint Conference on Artificial Intelligence, Morgan Kaufmann Publishers, Los Altos, CA, pp. 219-239, 1969. 5) McCarthy, J. and Hayes, P., "Some Philosophical Problems from the Standpoint of Artificial Intelligence," Machine Intelligence, Vol. 4 (B. Meltzer, D. Michie, eds.), Edinburgh University Press, Edinburgh, pp. 463-502, 1969. 6) Kowalski, R., Logic for Problem Solving, North-Holland, New York, Amsterdam, Oxford, 1979. 7) Bibel, W., "A deductive solution for plan generation," New Generation Computing, Vol. 4, pp. 115-132, 1986. 8) ~Fronh6fer, B., "Linearity and Plan Generation," New Generation Computing, Vol. 5, pp. 213-225, 1987. 9) Bibel, W., del Cerro, L. F., Fronhffer, B., and Herzig, A., "Plan Generation by Linear Proofs: on Semantics," in Proceedings of the German Workshop on Artificial Intelligence, Springer-Verlag, 1989. 10) Waldinger, R., "Achieving Several Goals Simultaneously," Machine Intelligence, Vol. 8, Elsevier Publishing Company, 1977. 11) Sheperdson, J. C., "Negation as Failure: A Comparison of Clark's Complete Data Base and Reiter's Closed World Assumption," Journal of Logic Programming, Vol. 1, No. 1, ppl 51-79, 1984. 12) Gallier, J. H. and Raatz, S., "Extending SLD-Resolution to Equational Horn Clauses Using E-Unification," Journal of Logic Programming, Vol. 6, pp. 3-44, 1989. 13) Hflldobler, S., Foundations of Equational Logic Programming, Vol. 353, LNCS, Springer-Verlag, 1989. 14) Siekmann, J., "Unification Theory," in Proceedings of the European Conference on Artificial Intelligence, pp. 365-400, 1986. 15) Lloyd, J. W., Foundations of Logic Programming, Springer-Verlag, 1984. 16) Sussman, G. J., A Computer Model of Skill Acquisition, Elsevier Publishing Company, 1975. 17) Reiter, R., "Orl closed world data bases," in Proceedings of the Workshop oh Logic and Databases (N. Gallaire, ed.), 1977. 18) Jaffar, J., Lassez, J.-L., and Maher, M. J., "A Theory of Complete Logic Programs with Equality," in Proceedings of the International Conference on Fifth Generation Computer Systems, pp. 175-184, 1984. 19) Jaffar, J., Lassez, J.-L., and Maher, M. J., "A Logic Programming Language Scheme," Logic Programming (DeGroot, Lindstrom, eds.), Prentice Hall, pp. 441-467, 1986. 20) Warren, D. H. D., "An Abstract Prolog Instruction Set," Technical Note 309, Stanford Research Institute (SRI), 1983. 21) Bfirckert, H. J., "Lazy Theory Unification in Prolog: An Extension of the Warren abstract machine," in Proceedings of the German Workshop on Artificial Intelligence,

244

S. HSlldobler, and J. Schneeberger

pp. 277-288, 1986. Swartout, W.(ed.), "DARPA Santa Cruz Workshop on Planning," A1 Magazine, pp. 115-130, Summer, 1988. 23) Kowalski, R., "Logic Programming," in Proceedings of the World Computer Congress of the IFIP, pp. 133-145, 1983. 24) Kowalski, R., "Directions of Logic Programming," in Proceedings of the Symposium on Logic Programming, Computer Society, Press of the IEEE, Washington, pp. 2-7, 1985. 25) Buntine, W. L. and BOrckert, H.-J., "On Solving Equations and Disequations," Technical Report, FB Informatik, Universit~t Kaiserslautern, 1989. 22)