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 quantification over situation terms. Although such queries arise naturally in many important reasoning tasks, they are difficult 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-quantified 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 fixpoint calculation; crucially, this calculation uses only first-order reasoning with a limited set of axioms. The result is a powerful new tool for verifying sophisticated domain properties in the situation calculus.