In this paper, we view planning as a special case of reasoning about indefinite actions. We treat actions as predicates defined over a linear temporal order. This formalism permits the representation of concurrent activpose we have a set of abstract actions defined by Horn clauses from a set of basic actions. Let us assume that an abstract action has occurred, and ask whether a given condition is entailed by all the basic actions that constitute . A countermodel to this hypothetical implication is then a plan for "doing and avoiding ." We propose a formalization of this problem using circumscription, and argue that this is the correct formalization if our action definitions include recursive rules. We then investigate two techniques for solving the problem: (1) a special type of inductive proof procedure, which is sound but not complete; and (2) a decision procedure that works for an interesting subclass of the general problem. Because of the use of recursive rules in our...
L. Thorne McCarty, Ron van der Meyden