Ryan F. Kelly, Adrian R. Pearce
We develop an algorithm for reducing universally quantified situation calculus queries to a form more amenable to automated reasoning. Universal quantification in the situation calculus requires a second-order induction axiom, making automated reasoning difficult for such queries. We show how to reduce queries about property persistence, a common family of universally-quantified query, to an equivalent form that does not quantify over situations. The algorithm for doing so utilizes only first-order reasoning. We give several examples of important reasoning tasks that are facilitated by our approach, including checking for goal impossibility and reasoning about knowledge with partial observability of actions.
Subjects: 3. Automated Reasoning; 1.11 Planning
Submitted: Oct 10, 2006