Property Persistence in the Situation Calculus

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

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.