--- title: "STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving" authors: - "Richard Fikes" - "Nils J. Nilsson" doi: "" url: "https://ijcai.org/proceedings/1971/63" pdf: "https://ijcai.org/proceedings/1971/0063.pdf" venue: "Proceedings of the Second International Joint Conference on Artificial Intelligence" year: 1971 pages: "608-619" track: "" keywords: --- # STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving Richard Fikes, Nils J. Nilsson *Proceedings of the Second International Joint Conference on Artificial Intelligence*, pages 608-619. ## Abstract We describe a new problem solver called STRIPS that attempts to find a sequence of operators in a space of world models to transform a given initial world model into a model in which a given goal formula can be proven to be true. STRIPS represents a "·orld model as an arbitrary collection of first-order predicate calculus formulas and is designed to work "·ith models consisting of large numbers of formulas. It employs a resolution theorem prover to answer questions of particular models and uses means-ends analysis to guide it to the desired goal-satisfying model. ## Full text STRIPS: A NEVi APPROACH TO niE APPLICATION OF THEOREM PROVING TO PROBLEM SOLVING Richard E. Fikes Nils J. Nilsson Stanford Research Institute Menlo Park, California u.s.A. ## ABSTRACT We describe a new problem solver called STRIPS that attempts to find a sequence of operators in a space of world models to transform a given initial world model into a model in which a given goal formula can be proven to be true. STRIPS represents a "·orld model as an arbitrary collec­ tion of first-order predicate calculus formulas and is designed to work "·ith models consisting of large numbers of formulas. It employs a resolu­ tion theorem prover to answer questions of partic­ ular models and uses means-ends analysis to guide it to the desired goal-satisfying model. ## DESCRIP'TIVE TERMS Problem solving, theorem provin~, robot planning, heuristic search. ## I STRODL'CT I OS This paper describes a new problem-solving program called STRIPS (STanford Research Institute Problem Solver). An initial ver;1on of the pro­ gram has-been implemented 1n LISP on a PDP-10 and is being used in conjunction ,..i th robot research at SRI. STRIPS is a member of the class of prob­ lem solvers that search a space of ""·orld models" to find one in which a g1ven goal is achieved. For any world model, "e assume that there exists a set of applicable operators, each of which trans­ forms the "·orld model to some other "·orld model. The task of the problem solver IS to find some composition of operators that transforms a given initial "orld model into one that satisfies some stated goal condition. This frame,.·ork fur problem solving has been central to much of the research in artificial intelligence (1). Our primary interest here is in the class of problems faced by a robot in re­ arranging obJects and in navlgatinl(, i.e., problems that require quite complex and ~eneral world models compared tu those needed in the solution of puzzles and ~(ames. In puzzles and games, a simple matrix or Jist structur<· is usually adequate to represent a state of th~· problem, The "·orld model for a robot problem sol\·er, ho,.ever, must include a large number of facts and relations dealin~ "·ith the posi­ tion of the robo t and the positions and attributes of vanous obJects, open spaces, and boundaries . Jn STHIPS, a "''rld model is representt·d by a set of "t·ll-formt·d formulas (wffs) 01 the first-order Pl'erllcate calculus . Operators are the basic elements .from which a solution is built. For robot problems, each operator corresponds to an action routine· "·hose execution causes a robot to~certain actions. For example, we might have a routine that causes it to go through a doorway, a routine that causes it to push a box, and perhaps dozens of others. Green (4) implemented a problem-solving system that depended exclusively on formal theorem­ proving methods to search for the appro.priate sequence of operators. While Green's formulation represented a significant step in the development of problem-solvers, it suffered some serious dis­ advantages connected v.·ith the "frame problem"+ that prevented 1t from solving nontrivial problems. In STRIPS, we surmount these difficulties by separating entirely the processes of theorem proving from those of searching through a space of world models. This separation allo,.·s us t o employ separate strategies for these two activities and thereby improye the overall performance of the system. Theorem-proving methods are used only within a given world model to answer ques­ tions""""BbbU't it concerning vchich operators are applicable and v.·hether or not goals have been satisfied. For searching through the space of world models, STRIPS uses a GPS-like means-ends analysis strategy (6). ThiS combination of means-ends analysis and formal theorem-proving methods allows objects (v.·orld models) much more complex and gen­ eral than any of those used in GPS and provides more powerful search heuristics than those found in theorem-proving programs. We proceed by describing the operation of STRIPS 1n terms of the conventions used to rep­ resent the search space for a problem and the search methods used to find a solution. Vie then discuss the details of implementation and present some examples. ·The reader should keep in mind the distinction between an operator and its associ a ted ~ routine. Execution of action routines actually causes the robot to take actions. Application of operators to world models occurs during the planning (i.e., problem solving) phase ··hen an attempt is being made to find a sequence of operators whose associated action routines ,..ill produce a desired state of the world. (See the papers by Munson (2) and Fikes (3) for discus­ sions of the relationships between STRIPS and the robot executive and monitoring functions . +Space does not allow a full discussion of the frame problem; for a thorough treatment, see Ref . (5). ## II THE OPERATION OF STRIPS R. E. FTKES, N.J . NILSSOX that there is an instance of the corrcspon<lin~ v.·ff schema that lo~ically follows from the model. ## A. The Problem Space The problem space for STRIPS is defined by the initial world model, the set of available opera­ tors and their effects on world models, and the goal statement. As already mentioned, STRIPS represents a world model by a set of well-formed formulas (wffs). For example, to describe a world model in v.·hich the robot is at location a and boxe~ B and C arc at location~ b and c we would inc}ude the following wffs: ATR(a) AT(B, b) AT(C,c) We might also include the wff to state the general rule that an object in one place is not in a different place. Using first-order predicate calculus wffs, we can represent quite complex world models and can use existing theorem­ proving programs to answer questions about a model. The available operators are grouped into fam­ ilies called schemata. Consider for example the operator goto for moving the robot from one point on the floo;:-to another. Here there is really a distinct operator for each different pair of points, but it is convenient to group all of these into a family goto(m,n) parameterized by the initial position· m and the final position n. We say that goto(m,n) is an operator schema whose members are obtained by substituting speci­ fic constants for the parameters m and n. In STRIPS, when an operator is applied to a world model, specific constants will already have been chosen for the operator parameters. Each operator is defined by an operator descrip­ tion consisting of two main parts: a description of the effects of the operator, and the conditions under which the operator is applicable. The effects of an operator are simply defined by a list of wffs that must be added to the model and a list of wffs that are no longer true and therefore must be deleted. We shall discuss the process of calcula­ ting these effects in more detail later. It is convenient to state the applicability condition, or precondition, for an operator schema as a wff schema. To determine whether or not there is-an instance of an operator schema applicable to a world model, we mu.st be able to prove For example, consider the question of applyifll.: instances of the operator subschema ~oto(m,b) to a world model containing the wff ATII(a\ whcr·c a and b are constants. If the precun<li tion v.·ff schema of goto(m, n) is ATR(m), then we find that the instance ATR(a) can be proved from the world model. Thus, an applicable instance of goto(m,h) is goto(a, b). · The parameters m and n are each really vectorvalued, but we avoid vector notation here for simplicity. In general, we denote constants by letters near the beginning of the alphabet (a,b,c, ··. ),\_ parameters by letters in the middle of the alphabet (m, n, ... ) , and quantified vari­ ables by letters near the end of the alphabet (x, y, z). It is important to distin~uish between the parameters appearing in wff schemata and ordinary existentially and universally quantified variables that may also appear. Certain modifications must be made to theorem-proving programs to enable them to handle wff schemata; these are discussed later. Goal statements are also represented by ··ffs. For example, the task "Get Boxes B and C to Loca­ tion a" might be stated as the wff: To summarize, the problem space for STRIPS is defined by three entities: - (l) An initial world model, which is a set of wffs describing the present state of the world. - (2) A set of operators, including a descrip­ tion of their effects and their precon­ dition wff schemata. - (3) A goal condition stated as a wff. The problem is solved when STRIPS produces a world model that satisfies the goal wff. ## B. The Search Strategy In a very simple problem-solving system, we might first apply all of the applicable operators to the initial world model to create a set of successor models. We would continue to apply all applicable operators to these successors and to their descendants (say in breadth-first fashion) until a model was produced in which the goal formula was a theorem. However, since we envision uses in which the number of operators applicable to any given world model might be quite large, such a simple system would generate an undesirably large tree of world models and would thus be impractical. Instead, we have adopted the GPS strategy of extracting "differences" between the present world model and the goal and of identifying operators that are "relevant" to reducing these differences (6). Once a relevant operator has been determined, we attempt to solve the subproblem of producing a world model to which it is applicable. If such a model is found, then we apply the relevant oper­ ator and reconsider the original goal in the resulting model. In this section, we review this basic GPS search strategy as employed by STRIPS. ## R. E. FIKES, N. J. NILSSON STRIPS begins by employing a theorem prover to attempt to prove that the goal wff G 0 follows from the set M of wffs describing the initial world model. 9f G 0 does follow from M 0 , the task is trivially solved in the initial model. Other­ wise, the theorem prover will fail to find a proof. In this case, the uncompleted proof is taken to be the "difference'' between Mo and G 0 · Next, operators that might be relevant to "redu­ cing" this difference are sought. These are the operators whose effects on world models would enable the proof to be continued. In determining relevance, the parameters of the operators may be partially or fully instantiated. The correspond­ ing instantiated precondition wff schemata (of the relevant operators) are then taken to be new subgoals. Consider the trivially simple example in which the task is for the robot to go to location b. The goal wff is thus ATR(b), and unless the robot is already at location b, the initial proof attempt will be unsuccessful, Now, certainly the instance goto(m,b) of the operator goto(m,n) is relevant to reducing the difference because its effect would allow the proof to be continued (in this case, completed). Accordingly, the corresponding precondition wff schema, say ATR(m), is used as a subgoal. STRIPS works on a subgoal using the same tech­ nique. Suppose the precondition wff schema G is selected as the first subgoal to be worked on. STRIPS again uses a theorem prover in an attempt to find instances of G that follow from the ini­ tial world model M 0 . Here again, the.re are two possibilities . If no proof can be found, STRIPS uses the incomplete proof as a difference, and ~ets up (sub) subgoals corresponding to their precondition wffs. If STRIPS does find an in­ stance of G that follows from M 0 , then the cor­ responding operator instance is used to transform Mo into a new world model M 1 · In our previous simple example, the subgoal wff schema G was ATR(m), If the initial model contains the wff ATR(a), then an instance of G--namely ATR(a)--can be proved from M 0 . In this case, the correspond­ ing operator instance goto(a, b) is applied to M 0 to produce the new model, M1. STRIPS then con­ tinues by attempting to prove Go from M 1 · In our example, G 0 trivially follows from M 1 and ~<·e are through. However, if no proof could be found, subgoals for this problem would be set up and the process would continue. The hierarchy of goal, subgoals, and models generated by the search process is represented by a search tree. Each node of the search tree has th;-rorm <(world model ) , (goal list)), and repre­ sents the problem of trying to achieve the sub­ goals on the goal list (in order) from the indi­ cated world model. An example of such a search tree is shown in Figure 1. The top node (M 0 , (G 0 )) represents the main task of achieving goal G 0 from world model M 0 · In this case, two alternative subgoals Ga and Gb are set up. These are added to the front of the goal lists in the two successor nodes . Pursuing one of these subgoals, suppose that in the node (M 0 ,<Ga,Go>>, goal Ga is satisfied in M 0 ; the corresponding operator, say OPa, is then applied to M 0 to yield M 1 . Thus, along this branch, the problem is now to satisfy goal Go from M 1 , and this problem is represented by the node (M 1 ,<Go)). Along the other path, suppose Gc is set up as a subgoal for achieving Gb and thus the node (M 0 ,<Gc,Gb,G 0 )) is created. Suppose Gc is satisfied in M 0 and thus OPe is applied to Mo yielding M 2 . Now STRIPS must still solve the subproblem Gb before attempting the main goal G 0 . Thus, the result of applying OPe is to replace Mo by M 2 and to remove Gc from the goal list to produce the node (M 2 , (Gb,Go>>. This process continues until STRIPS produces the node (M4 , (G 0 )). Here suppose G 0 can be proved directly from M 4 so that this node is terminal. The solution ·sequence of operators i s thus (OPc,OPb,OPe). This example search tree indicates clearly that when an operator is found to be relevant, it is not known where it will occur in the com­ pleted plan; that is, it may be applicable t o the initial model and therefore be the first operator applied, its effects may imply the goal so that it is the last operator applied, or it may be some intermediate step to~<· ard the goal. This flexible search strategy embodied in STRIPS combines many of the advantages o f both fo r~<ard search (from the initial model toward the goal) and backward search (from the goal toward the initial model). 1\'henever STRIPS generates n successor node, it immediately tests to sec if th<' first goal o n the goal list is satisfied in the new node's model. If so, the corresponding operator is applied, generating a new successor node ; if no t, the difference (i.e., the uncompleted proof) 1s stored with the node. Except for those successor nodes generated as a result of applying operators, the process of successor generation is as follo~<s : STRIPS selects a node and uses the difference stored with the node to select a relevant opera­ tor. It uses the precondition of this operator to generate n new successor. (Jf all of the node 's successors have nl rendy been generated, STHIPS selects some other node still having uncompleted successors.) A flowcha··t summarizing the STHIPS search process is shown in Figure :! . STRIPS has a heuristic mechanism to select nodes with uncompleted successors to ~ork on next. Fo·· this purpose we usc an cvalu:Jt inn func­ tion that takes into account such facto1·s as the number of ··cmaining goals on the goal list, till' number and types of predicates in the rcmainin~: go:Jl formulas, :1nd the complcxi ty of the eli ffercnc e attached to the node. FIGURE 2 flOW CHART FOR STRIPS ![Image](https://ijcai.org/proceedings/1971/fulltext/63/image_000000_fedb7a074ccd4767b7b78eaf5fdef4e56c77e0c68c29f99280e3c24c9b0ae262.png) ## III IMPLEMENTATION ## A. Theorem-Proving with Parameters In this section, we discuss the more impor­ tant details of our implementation of STRIPS; we begin by describing the automatic theorem-proving component. ## R. E. FIKES, N. J. NILSSON We next need a W&¥ to state the e ·ffects of operator application on world models. These effects are simply described by two lists. On the delete list we specify those clauses in the original model that might no longer be true in the new model. On the add list are those clauses that might not have be;;-t~in the original model but are true in the new model. STRIPS uses the resolution theorem-prover QAJ.5 (7) when attempting to prove goal and sub­ goal wffs. We assume that the reader is familiar with resolution proof techniques for the predicate calculus (1). These techniques must be extended to handle the parameters occurring in wff schemas; we discuss these extensions next. The general situation is that we have some goal wff schema G(p), say, that is to be proved from a set M of clauses where p is a set of schema parameters. Following the general strategy of resolution theorem provers, we attempt to prove the inconsistency of the set (M U- G(p)} . That is, we attempt to find an instance p' of ~ for which (M U - G(p')} is inconsistent. We have been able t o use the standard unifi­ cation algorithm of the resolution method to com­ pute the appropriate instances of schema variables during the search for a proof. This algorithm has the advantage that it finds the most general instances of parameters needed to effect unifica­ tion. To use the unification algorithm we must specify how it is to treat parameters. The follow­ ing substitution types are allowable components of the output of the modified unification algorithm: - Terms that can be substituted for a var­ iable: variables, constants, parameters, and functional terms not containing the variable. - Terms that can be substituted for a param­ eter : constants, parameters, and func­ ~al terms no t containing Skolem func­ tions, variables, or the parameter. The fact that the same parameter may have multiple occurrences in a set of clauses demands another modificati on to the theorem prover. Suppose two clauses c 1 and c 2 resolve to form clause C and that in the process some term t is substituted for parameter p. Then we must make sure that p is replaced by t in all of the clauses that are descendants of C. ## B. Operator Descriptions and Applications We have already mentioned that to define an operator, we must state the preconditions under which it is applicable and its effects on a world model schema. Preconditions are stated as wff schemata. For example, suppose G(p) is the oper­ at o r preconditi on schema of an operator O(p), p is a set of parameters, and M is a world model. Then if p' is a constant instance of p for which {M ~ - G(p') } i s contradictory, then STRIPS can apply operator O(p') to world model M. For example, consider an operator push(k,m,n) for pushing object k from m to n. Such an oper­ ator might be described as follows: ## push(k,m, n) | Precondition : | ATR(m) A AT(k, m) | |------------------|---------------------| | delete list | | | | ATR(m) ; | | | AT(k, m) | | add list | | | | ATR(n); | | | AT(k, n) | The parameters of an operator schema are instantiated by constants at the time of opera­ tor application. Some instantiations are made while deciding what instances of an operator schema are relevant to reducing a difference, and the rest are made while deciding what instances of an operator are applicable in a given world model. Thus, when the add and delete lists are used to create new world models, all parameters occurring in them will have been replaced by con­ stants. (We can make certain modifications to STRIPS to allow it to apply operators with uninstantiated parameters. These applications will produce wo rld model schemata. This generalization complicates somewhat the simple add and delete-list rules for computing ne.,.· world models and needs further study.) For certain operators it is convenient to be able merely to specify the form of clauses to be deleted . For example, one of the effects of a robot goto operator must be to delete information about ~direction that the robot was originall y facing even though such information might not have been represented by one of the parameters o f the operator. In this case we would include the atom FACING($) on the delete list of goto with the convention that any atom of the !~FACIN�($), regardless of the value of $, would be deleted. When an operator description is written, it may not be possible to name explicitly all the atoms that should appear on the delete list. For example, it may be the case that a world model contains clauses that are derived from other clauses in the model. Thus, from AT(Bl,a) and from AT(B2, a · 6), we might derive NEXTTO(Bl, B2) and insert it into the model. Now, if one of the clauses on which the derived clause depends ## R. E. FIKES, S. J. NILSSOS is deleted, then the derived clause must also be deleted. 1\"e deal "i th this problem by dcfininp: a set of primitive predicates (e.g,, AT, ATR) and relating all other predicates to this primitive set. In particular, v.·e require the delete list of an operator description to indicate all the atoms containing primitive predicates that should be deleted when the operator is applied. Also, we require that any nonprimitive clause in the world model have associated with it those primi­ tive clauses on which its validity depends. (A primitive clause is one which contains only prim­ itive predicates.) For example, the clause ~'EXTTO(Bl, B2) would have associated with it the clauses AT(Bl,a) and AT(B2,a · ~). By using these conventions, we can be assured that primitive cl;~uses will be correctly deleted dur1ng operator applications, and that the valid­ ity of nonprimitive clauses can be determined whenever they are to be used in a deduction by checking to see if all of the primitive clauses on which the nonprimitive clause depends are still in the world model. ## C. Computing Differences and Relevant Operators STRIPS uses the GPS stratep:y of attempting to apply those operators that are relevant to redu­ cing a difference between a world model and a goal or subgoal. 1\"e use the theorem prover as a key part of this mechanism, Suppose we have just created a new node in the search tree represented by Ot, (Gi,Gi-1· ... , Go)). The theorem prover is called to attempt to find a cant radiction for the set ~~~ ~- Gi } . If one can be found, the operator whose precondition was Gi is applled to ~~ and the process continues. Here, though, we are ·interested in the case in which no contradiction is obtained after investing some prespecified amount of theorem­ proving effort, The uncompleted proof Pis represented by the set of clauses that form the negation of the goal v.·ff, plus all of their descendants (if any), less any clauses eliminated by editing strategies (such as subsumption and predicate evaluation). 1\"e take P to be the dif- · ference between ~~ and G 1 and attach P to the node. Later, 1n attempting to compute a successor to this ·node with incomplete proof P attached, we first must select a relevant operator. The quest for relevant operators proceeds in two steps. In the first step an ordered list of candidate operators is created. The selection of cand1date operators is based on a simple com­ parison of the predicates in the difference clauses with those on the add l1sts of the operator dcscr·iptions. For· example, 1 f the di ffercnce contained a clause havin~ in it the nep:at1on of a position predicate AT, then the operator push would be considered as a candidate for this-­ difference. · If P is very large we can heuristically select some part of P as the difference. The second step in finding an operator rele­ vant to a given difference involves employing the theorem prover to determine if clauses on the add list of a candidate operator can be used to "resolve away" clauses in the difference (i.e., to sec if the proof can be continued based on the effects of the operator). If the theorem prover can in fact produce new resolvents that are descendants of the add list clauses, then the candidate operator (properly instantiated) is considered to be a relevant operator for the difference set. Sate that the consideration of one candidate operator schema may produce several relevant operator instances. For example, 1 f the differ­ ence set contains the unit clauses -ATRia) and - ATR(b) 1 then there are t...·o relevant instances of goto(m,n), namely goto(m,a) and goto(m,b). Each new resolvent that is a descendant of the operator's add list clauses is used to form a relevant instance of the operator by applying to the operator's parameters the same substitutions that were made during the production of the resolvent. ## D. Efficient Representation of 1\"orld ~lodels A primary design issue in the implementation of a system such as STRIPS is how to satisfy the storage requirements of a search tree in which each node may contain a different world model, 1\'e would like to use STRIPS in a robot or questionanswering environment v.·here the in1tial model may consist of hundreds of wffs, applications it is infeasible to recopy world For such completely a world model each time a new model is produced by application of an operator. 1\'e have dealt with this problem in STRIPS by first assuming that most of the wffs in a prob­ lem's initial world model will not be changed by the application of operators. This is cer­ tainly true for the class of robot problems with which we are currently concerned. For these problems most of the wffs in a model describe rooms, walls, doors, and objects, or specify general properties of the world, which are true in all models, The only wffs that might be changed in this robot environment are the ones that describe the status of the robot and any objects which it manipulates. Given this assumption, we have implemented the following scheme for handling multiple world models. All the wffs for all world models are stored in a common memory structure. Associated with each wff (i.e., clause) is a visibility flag, and QA3,5 has been modified to consider only clauses from the memory structure that are marked as visible. Hence, we can "define" a ## R. E. FIKES, N. J, NILSSON particular world model for QAJ.S by marking that model's clauses visible and all other clauses invisible. When clauses are entered into the initial world model, they are all marked as vis­ ible. Clauses that are not changed remain visible throughout STRIPS' search for a solution. Each world model produced by STRIPS is defined by two clause lists. The first list, DELETIONS, names all those clauses from the initial world model that are no longer present in the model being defined. The second list, ADDITIONS, names all those clauses in the model being defined that are not also in the initial model. These lists represent the changes in the initial model needed to form the model being defined, and our assump­ tion implies they will contain only a small number of clauses. To specify a given world model to QA3.5, STRIPS marks visible the clauses on the model's ADDITIONS list and marks invisible the clauses on the model's DELETIONS list. When the call to QAJ.S is com­ pleted, the visibility markings of these clauses are returned to their previous settings. When an operator is applied to a world model, the DELETIONS list of the new world model is a copy of the DELETIONS list of the old model plus any clauses from the initial model that are deleted by the operator. The ADDITIONS list of the new model consists of the clauses from the old model's ADDITIONS list, as transformed by the operator, plus the clauses from the operator's add list. ## E. An Example Tracing through the main points of a simple example helps to illustrate the various mechan­ isms in STRIPS. Suppose ,..e want a robot to gather together three objects and that the ini­ tial world model is given by : The goal wff describing this task is Its negated form is (In- G 0 , the term x is a universally quantified variable.) We admit the following operators: - (l) push(k,m,n): Robo t pushes object k !roc place m to place n. Precondition: AT(k,m) 1\ ATR(m) Negated precondition: AT(k,m) v-ATR(m) Delete list: ATR(m) AT(k,m) Add list: AT(k,n) ATR(n) - (2) goto(m,n): Robot goes from place m to place n. Precondition: ATR(m) Negated precondition: - ATR(m) . Delete list: Add list: ATR(m) ATR(n) Following the flow chart of Fig. 2, STRIPS first creates the initial node (Mo, (Go)) and attempts to find a contradiction to (M 0 U - G 0 } . This attempt is unsuccessful; suppose the incom­ plete proof is: ![Image](https://ijcai.org/proceedings/1971/fulltext/63/image_000001_a2fa81e61ad24f2d4644321823d06491ec14bfb0ed43952029bf1ee8de2d91a9.png) We attach this incomplete proof to the node and then select the node to have a successor computed. The only candidate operator is push(k,m,n) . l 1 s ing the add list clause AT(k, n), we can con­ tinue the uncompleted proof in one of several ways depending on the substitutions made f o r k and n. Each of these substitutions produces a relevant instance of push. One of these is : given by the substitutions BOX2 for k and b f or n. Its associated precondition (in negated f o rm) is: Suppose OP 1 is selected and used to create a successor node. (Later in the search process another successor using one of the other rele­ vant instances of push m1ght be computed if our original selection did no t lead t o a solution . ) Selecting OP 1 leads to the computation of the successor node (~1 1 ,, <G 1 ,G 0 )). STRIPS next attempts to find a contradiction for ; ~lu ~ - G 1 ! . The incompleted proof (differ­ ence) attached to the node contains : ![Image](https://ijcai.org/proceedings/1971/fulltext/63/image_000002_f84e9ea6c44576348382e9213dc1f7ffba8e70a12f52de0da54616242aad7224.png) R. ~. FIKES, N. J. NILSSON When this node is later selected to have a suc­ cessor computed, one of the candidate operators is goto(m,n). The relevant instance is determined to be with (negated) precondition This relevant operator results in the successor node (M 0 , (G 2 ,G 1 ,G 0 )) . Next STRIPS determines that (M 0 U - G 2 ) is contradictory with m = a. Thus, STRIPS applies the operator goto(a,c) to Mo to yield The successor node is (M 1 ,(G 1 ,Gg)) . Immediately, STRIPS determines that (M 1 'J - 1 ) is contradic­ tory with m = c. Thus, STRIPS applies the oper­ at o r pus·h(BOX2,c, b) to yield The resulting successor node is (M 2 , (G 0 )), and thus STRIPS reconsiders the original problem but no··· beginning with world model M 2 · The rest of the solution proceeds in similar fashion, Our implementation of STRIPS easily produces the solution {goto(a,c),push(BOX2,c,b), goto(b,d), push( OOX3, d, b) } . (Incidentally, Green's theorem· prov ing problem-solver (4) has not been able to obtain a solution to this ·version of the 3-Boxes pro blem. It did s o lve a simpler version of the pro blem designed to require only two operator applicati ons.) ## IV EXAMPLE PROBLEMS SOLVED BY STRIPS STRIPS has been designed to be a general­ purpose problem solver for robot tasks, and thus must be able to work with a variety of operators and with a world model containing a large number o f facts and relations . This section describes its perfo·rmance on three different tasks. The initial world model for all three tasks consists o f a corridor with four rooms and doorways (see Fig. 3) and is described by the list of axioms in Table l. Initially, the robot is in ROOMl at location e. Also in ROOM! are : A large box, BOXl at location a; two smaller boxes, OOX2 at l ocation b, and BOXJ at location c; and a light­ switch, LIGHTSWITCHl at location d. The light­ switch is high on a wall out of normal reach of the robot. The first task is to turn on the lightswitch. The robot can solve this problem by going to the largest of the three boxes, BOXl, pushing it to the lightswitch, climbing on the box* and turning on the lightswitch. The second task is to push the three boxes in ROOMl together. (This task is a more realistic elaboration of the three-box problem used as an example in the last section.) The third task is for the robot to go to a desig­ nated location, f, in ROOM4. The operators that are given to STRIPS to solve these problems are ~escribed in Table 1. For convenience we define two "goto" operators, gotol and goto2. The operator gotol(m) takes the robot to any coordinate location m in the same room as the robot. The operator goto2(m) takes the robot next to any item m (e.g., lightswitch, door, or box) in the sam~om as the robot . The oper­ ator pushto(m,n) pushes any pushable object m next to any item n (e.g,, lightswitch, door or box) in the g;;; room as the robot. Additionally, we have operators for turning on lightswitches, going through doorways, and climbing on and off boxes. The precise formulation of the preconditions and the effects of these operators is contained in Table 1. We also list in Table 1 the goal wffs for the three tasks and the solutions obtained by STRIPS. Some performance figures for these solutions are shown in Table 2. In Table 2, the figures in the "Time Taken" column represent the CPU time (excluding garbage collection) used by STRIPS in finding a solution. Although some parts of our program are compiled, most of the time is spent running interpretive code ; hence, we do not attach much importance to these times . We note that in all cases most of the time is spent doing theorem proving (in QA3.5). The next columns of Table 2 indicate the number of nodes generated and the number of oper­ ator applications both in the search tree and along the solution path. (Recall from Fig . 2 that some successor nodes do not correspond to operator applications.) We see from these figures that the general search heuristics built into STRIPS provide a highly directed search toward the goal. These heuristics presently give the search a large "depth-first " component, and for this reason STRIPS obtains an interesting but nonoptimal solution to the "turn on the light­ switch" problem. · This task is a robot version of the. so-called ·~onkey and Bananas" problem. STRIPS can solve the problem even though the current SRI robot is incapable of climbing boxes and turning on lightswitches · ## Initial World Model ``` CON!I"ECTS ( IX)()R 1, ROOM! , ROOMS) ACONJI."ECTS ( IX)()Rl, ROOMS ,ROOMl) CO!>!\"ECTS(DOOR2, ROOM2 ,ROOM5) t.CONJ\"ECTS (DOOR2 ,ROOMS, ROOM2) CONJ\"ECTS(IX)()RJ , ROOMJ ,ROOMS) 1\CO:.;!'."ECTS (DOORJ, ROOMS ,ROOMJ) CO:illo"ECTS(DOOR4 ,ROOM