The CAltAlt planner uses the regression operator to generate children in an A* search. Regression terminates when search node expansion generates a belief state which is logically entailed by the initial belief state . The plan is the sequence of actions regressed from to obtain the belief state entailed by .
For example, in the BTC problem, Figure 1, we have:
Regress DunkP1) = clog ( arm inP1).
The first clause is the execution formula and the second clause is the causation formula for the conditional effect of DunkP1 and arm.
Regressing with Flush gives:
Regress Flush ( arm inP1).
For , the execution precondition of Flush is , the causation formula is clog , and ( arm inP1) comes by persistence of the causation formula.
Finally, regressing with DunkP2 gives:
Regress DunkP2) = clog ( arm inP1 inP2).
We terminate at because . The plan is DunkP2, Flush, DunkP1.