...table

The concepts of final position and tower-deadlock will be defined formally later on.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...strategy

If we assume the existence of an initial situation 9#9, the problem of determining what sequences of actions may be selected according to a particular strategy can be seen as the problem of determining what situations are selectable for that strategy.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...4#4

The situational argument 4#4 in the predicates Good, Bad and Better allows reasoning about multiple goals. For example, by substituting the variable 4#4 by two different constants 5#5 and 6#6 we can express the fact that performing action a at situation s is good for the purpose of achieving the goal described by situation 5#5, but bad for achieving the goal described by situation 6#6.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...situation

The idea here is to select always the best possible action.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...achieved

We define 10#10 and Prec(a,s) formally later on. In general, a situation s achieves the goal described by another situation 4#4 if all the conditions (propositional fluents) that hold at 4#4 hold at s as well. Prec(a,s) is true if action a can be performed at situation s.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...)

In the paper, we use the expression ``propositional fluent'' and the word ``proposition'' to refer to the corresponding reified formula.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...symbols

The symbols h and g are meta-variables ranging over distinct function symbols; the expressions 16#16 and 17#17 represent tuples of variables.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...that

We use the following notation to abbreviate the description of situations 19#19, and 20#20, where l is a sequence of actions (i.e., sequences of actions are applied from left to right).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...values

The symbols 23#23 and 24#24 are syntactical variables ranging over block constants.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...30#30)

Notice the distinction between 31#31 (axiom ) and reachable 32#32 (axiom ). It is crucial for understanding the role of the goal situation 33#33 in the formalization. The fact that axiom implies that the goal situation 33#33 is not reachable from the initial situation 34#34 does not imply that the planning problem is not solvable. When the program selects an action (see axiom defining the fluent selectable), it tries to find a situation reachable from the initial situation at which the goal is achieved. That is, a situation that satisfies the conditions imposed on the goal situation. In this sense, we could say that the role of the goal situation 33#33 is purely descriptive, as far as this paper is concerned.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...partially

Axioms and are not explicit definitions of final and above, because these symbols occur both on the left and right hand sides. But these formulas are strong enough for deriving both positive and negative ground instances of Holds(Above(x,y),s) and Holds(Final(x,S36#36),s) from the positive and negative ground instances of Holds(On(x,y),s) that can be derived from axioms to . [Davis1990] points out that it is possible to define on in terms of beneath (37#37), but it is not possible to fully define beneath in terms of on in a first order theory.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...sets

In the following, we denote the universal closure of a formula A by A'.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...logic

Notice that the only second order axiom in 41#41 is an axiom of induction for situations, which we do not need to decide the selectability of a single situation.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...descriptions

The expression (strategy) can also be parameterized with respect to the problem description (axioms and ), the theory of action (axioms to ), or the mechanism for action selection (axiom ).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...strategies

A strategy is state-based if whether an action is good or bad for a given goal at a particular situation depends only on what holds at that situation (i.e. the state associated with that situation), and not on what situations or actions have been selected so far. All the strategies considered in the paper are state-based.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...HREF="node1.html#safe2">

Strategy-2 is defined, in fact, by two action selection rules. The first one is axiom , the second is as follows 57#57. This rule guarantees that the strategy terminates as shown in fig. . The rest of the strategies that terminate do not need this rule, because it is subsumed by axiom .

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...actions

It compares the maximum length of the solutions generated by strategies 4 and 5.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...bad

Notice that axiom implies Better(Move(A,F),Move(A,T),S36#36,S66#66).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.