Property persistence in the situation calculus

9 years 1 months ago
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.
Ryan F. Kelly, Adrian R. Pearce
Added 08 Dec 2010
Updated 08 Dec 2010
Type Journal
Year 2010
Where AI
Authors Ryan F. Kelly, Adrian R. Pearce
Comments (0)