The situation calculus: Decidability and an approach based on the logic for non-monotone inductive definitions.

摘要

The situation calculus is a logical language for reasoning about action and change. A reasoning problem for the situation calculus can be formulated as follows: Given a basic action theory $D$ and a query &phis; is &phis; a logical consequence of $D$? We demonstrate that the reasoning problem is decidable for a rather expressive fragment of the situation calculus. We allow second order quantification over finite and infinite sets of situations, as well as over some object variables. The complexity of the decision procedure is non-elementary. If arbitrary functions are allowed, the situation calculus becomes undecidable.; Motivated by the well-known complexity/expressiveness tradeoff, we develop a less expressive variant of the situation calculus. To achieve it, we go beyond the problems specific to the situation calculus. We introduce a Logic for Non-Monotone Inductive Definitions, which is based on the idea of Iterated Induction. This logic contributes to the theory of inductive definitions by giving a clear logical formalization of Iterated Induction. In addition, it provides a new tool for solving knowledge representation problems.; To use this tool effectively, we need to be able to combine and decompose definitions into sub-definitions. These two operations may change the original meanings of definitions. We study under what conditions combining and decomposing definitions is equivalence-preserving. These results imply another theorem, which is, when combined with previously known techniques, a powerful tool for reducing formulas with complex definitions to first-order formulas.; We introduce an inductive variant of the situation calculus, an discuss applications of our Logic to the semantics of ConGolog and to the verification of ConGolog programs. Then we use the results about equivalence-preserving combining and decomposing definitions to address the ramification problem, which is the question of how to represent indirect effects of actions. We describe a general solution in our inductive version of the situation calculus, and present a series of simplifications which hold under particular assumptions about the logical theory. Finally, we formulate a sufficient condition for obtaining first-order successor state axioms of the situation calculus.