H.: First-order strong progression for local-effect basic action theories

In a seminal paper Lin and Reiter introduced the notion of progression for basic action theories in the situation calculus. The idea is to replace an initial database by a new set of sentences which reflect the changes due to an action. Unfortunately, progression requires second-order logic in general. In this paper, we introduce the notion of strong progression, a slight variant of Lin and Reiter that has the intended properties, and we show that in case actions have only local effects, progres-sion is always first-order representable. Moreover, for a restricted class of local-effect axioms we show how to construct a new database that is finite