Progression of Decomposed Situation Calculus Theories

In many tasks related to reasoning about consequences of a logical theory, it is desirable to decompose the theory into a number of components with weakly-related or independent signatures. This facilitates reasoning when signature of a query formula belongs to only one of the components. However, an initial theory may be subject to change due to execution of actions affecting features mentioned in the theory. Having once computed a decomposition of a theory, one would like to know whether a decomposition has to be computed again for the theory obtained from taking into account the changes resulting from execution of an action. In the paper, we address this problem in the scope of the situation calculus, where change of an initial theory is related to the well-studied notion of progression. Progression provides a form of forward reasoning; it relies on forgetting values of those features which are subject to change and computing new values for them. We prove new results about properties of decomposition components under forgetting and show when a decomposition can be preserved in progression of an initial theory