Property persistence in the situation calculus

We develop a new automated reasoning technique for the situation calculus that can handle a class of queries containing universal quantication over situation terms. Although such queries arise naturally in many important reasoning tasks, they are dicult to automate in the situation calculus due to the presence of a second-order induction axiom. We show how to reduce queries about property persistence, a common type of universally-quantied query, to an equivalent form that does not quantify over situations and so is amenable to existing reasoning techniques. Our algorithm replaces induction with a meta-level xpoint calculation; crucially, this calculation uses only rst-order reasoning with a limited set of axioms. The result is a powerful new tool for verifying sophisticated domain properties in the situation calculus.

• Type: Journal
• Year: 2010
• Where: AI
• Authors: Ryan F. Kelly, Adrian R. Pearce
• Keywords: AI 2010, Artificial Intelligence, Important Reasoning Tasks, Reasoning Techniques, Second-order Induction Axiom