Reasoning About Indefinite Actions.
L. Thorne McCarty, Ron van der Meyden · 1992
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 activity. Suppose 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 OE is entailed by all the basic actions that constitute /. A countermodel to this hypothetical implication is then a plan for "doing / and avoiding OE." 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 i...