Regression in Modal Logic
Robert Demolombe* — Andreas Herzig** — Ivan Varzinczak**
* ONERA Toulouse
2 Avenue Edouard Belin, B.P. 4025
31055 Toulouse Cedex France
** Institut de Recherche en Informatique de Toulouse
118, route de Narbonne
31062 Toulouse Cedex 4 France
ABSTRACT. In this work we propose an encoding of Reiter’s Situation Calculus solution to the
frame problem into the framework of a simple multimodal logic of actions. In particular we
present the modal counterpart of the regression technique. This gives us a theorem proving
method for a relevant fragment of our modal logic.
KEYWORDS: reasoning about actions, regression, modal logic, dependence.
In the reasoning about actions field most approaches use the Situation Calculus
formalism [MCC 69]. Among those, Reiter’s [REI 91] has turned out to be most fruit-
ful. His basic formalism is restricted to deterministic actions without ramifications.
In order to solve the frame problem he makes use of so-called successor state axioms
(SSAs). The latter enable regression [REI 91], which has interesting computational
The Situation Calculus is a dialect of predicate logic, having situations and actions
as objects, and where actions are viewed as mappings on the set of situations. At first
glance this is very close to possible worlds semantics for Deterministic PDL [HAR 84].
But the precise relation between Reiter’s approach and dynamic logic is not as obvious
as that. One of the reasons why his formalism cannot be translated straightforwardly
into modal logics of action such as PDL is that the Situation Calculus allows quanti-
fying over actions. Worse, such quantifications are central to Reiter’s approach.
Journal of Applied Non-Classical Logics.Volume 13 – n◦ 2/2003, pages 165 to 185
Journal of Applied Non-Classical Logics. Volume 13 – n◦ 2/2003
In [DEM 03] there has been presented a technique to translate Reiter’s approach
into dynamic logic. In this paper we present a different app