We consider a modified version of the situation calculus built using a two-variable fragment of the first-order logic extended with counting quantifiers. We mention several additional groups of axioms that can be introduced to capture taxonomic reasoning. We show that the regression operator in this framework can be defined similarly to regression in Reiter’s version of the situation calculus. Using this new regression operator, we show that the projection and executability problems (the important reasoning tasks in the situation calculus) are decidable in the modified version even if an initial knowledge base is incomplete. We also discuss the complexity of solving the projection problem in this modified language in general. Furthermore, we define description logic based sub-languages of our modified situation calculus. They are based on the description logics ALCO(U) (or ALCQO(U), respectively). We show that in these sub-languages solving the projection problem has better computational complexity than in the general modified situation calculus. We mention possible applications to formalization of Semantic Web services and some connections with reasoning about actions based on description logics.
A Logic For Decidable Reasoning About Actions
