As an example, we formalize Sussman's anomaly problem within this framework. The individual variables x, y and z range over blocks. The constant blocks are A, B, C and T (for Table). The function On maps a pair of blocks x and y into the reified formula of the sort database On(x,y) describing the fact that block x is on block y. The function Move maps a pair of blocks x and y into the action Move(x,y) denoting the act of moving block x on top of block y. The precondition, delete list, and add list of Move(x,y) are described as follows.
Figure: Sussman's anomaly.
The conditions on the initial and goal situations ( and ) are respectively described by axioms and . The formula is true iff formula f is at location i in the stack describing .