Inductive Situation Calculus

Temporal reasoning has always been a major test case for knowledge representation formalisms. In this paper, we develop an inductive variant of the situation calculus using the Logic for Non-Monotone Inductive Definitions (NMID). This logic has been proposed recently and is an extension of classical logic. It allows for a uniform represention of various forms of definitions, including monotone inductive definitions and non-monotone forms of inductive definitions such as iterated induction and induction over well-founded posets. In the NMID-axiomatisation of the situation calculus, fluents and causality predicates are defined by simultaneous induction on the well-founded poset of situations. The inductive approach allows us to solve the ramification problem for the situation calculus in a uniform and modular way. Our solution is among the most general solutions for the ramification problem in the situation calculus. Using previously developed modularity techniques, we show that the basic variant of the inductive situation calculus without ramification rules is equivalent to Reiter-style situation calculus.

Authors

• Marc Denecker
• Eugenia Ternovska

Keywords

No keywords are indexed for this paper.