Towards an Expressive Practical Logical Action Theory

In the area of reasoning about actions, one of the key computational problems is the projection problem: to find whether a given logical formula is true afterperforming a sequence of actions. This problem is undecidable in the generalsituation calculus; however, it is decidable in some fragments. We considera fragment P of the situation calculus and Reiter's basic action theories (BAT)such that the projection problem can be reduced to the satisfiability problemin an expressive description logic $ALCO(U)$ that includes nominals ($O$),the universal role ($U$), and constructs from the well-known logic $ALC$. It turns outthat our fragment P is more expressive than previously explored description logicbased fragments of the situation calculus. We explore some of the logical properties of our theories.In particular, we show that the projection problem can be solved using regressionin the case where BATs include a general ``static" TBox, i.e., an ontology that hasno occurrences of fluents. Thus, we propose seamless integration of traditionalontologies with reasoning about actions. We also show that the projectionproblem can be solved using progression if all actions have only local effects onthe fluents, i.e., in P, if one starts with an incomplete initial theory thatcan be transformed into an $ALCO(U)$ concept, then its progression resulting fromexecution of a ground action can still be expressed in the same language. Moreover,we show that for a broad class of incomplete initial theories progression can be computed efficiently.