From axioms to , we can prove , and , which allow us to derive the solution.

In STRIPS the goal stack contains both subgoals and actions that have been proposed to satisfy those subgoals. Therefore, subgoals are indexed both by their location in the goal stack, and by the actions that are above them in the stack. We describe such indexical information using variables for locations (i, j, k, ...), and representing subgoals by quoted formulas of the following sorts Quote(DB(p,s)) or Quote(Prec(a,s)). The situation argument s allows us to keep track of the situation with respect to which each subgoal should be satisfied (i.e., of the actions that are above it in the goal stack).