state 1:

ENABLE clearA onAC => -onAC ontableA clearC

ENABLE onBA clearB => -onBA ontableB clearA

ENABLE onBC clearB => -onBC ontableB clearC

ENABLE onCA clearC => -onCA ontableC clearA

state 2:

ENABLE onBA clearC clearB => -onBA -clearC onBC clearA

ENABLE clearA onAC => -onAC ontableA clearC

ENABLE ontableB clearC clearB => -ontableB -clearC onBC

state 3:

ENABLE onAB clearA => -onAB ontableA clearB

ENABLE clearA onAC => -onAC ontableA clearC

ENABLE onCA clearC => -onCA ontableC clearA

ENABLE onCB clearC => -onCB ontableC clearB

state 4:

ENABLE clearA onAC => -onAC ontableA clearC

ENABLE onCB clearC => -onCB ontableC clearB

ENABLE ontableA clearA clearB => -ontableA -clearB onAB

ENABLE ontableB clearC clearB => -ontableB -clearC onBC

Figure 7: Enabled operators for each state

## Acknowledgements

This research was funded by the Deutsche Forschungsgemeinschaft SFB 527. The author also wishes to thank the Finnish Cultural Foundation and the Finnish Academy of Science and Letters for additional nancial support. Holger Pfeifer kindly helped with proof-reading.

## Appendix A: Sample Plans

Sample plans found by our theorem-prover are given below. In the rst problem with three blocks, the goal is to have on and on C. The initial states are all the possible congurations of the three blocks. The plan encoding is the one described in Section 4.2.1 and it has four states. In each state a number of operators are enabled, as described in Figure 7. The execution of the plan starts from state 1, and the goal is reached at time 4.

At every point of time a transition to a successor state is made on the basis of truth-values of facts conXY that are dened by conXY onXY clearX). The transition function is given in Table 4. In all executions of the plan, transitions through the same sequence 1,3,2,4 of states are made.

The second problem instance has four blocks. We give a plan obtained with the encoding in Section 4.2.2. The goal is to have on B, on C, and on D. The initial states are
