Abstract In a seminal paper, Lin and Reiter introduced the notion of progression for basic action theories in the situation calculus. Unfortunately, progression is not fifirst-order defifinable in general. Recently, Vassos, Lakemeyer, and Levesque showed that in case actions have only local effects, progression is fifirstorder representable. However, they could show computability of the fifirst-order representation only for a restricted class. Also, their proofs were quite involved. In this paper, we present a result stronger than theirs that for local-effect actions, progression is always fifirst-order defifinable and computable. We give a very simple proof for this via the concept of forgetting. We also show fifirst-order defifinability and computability results for a class of knowledge bases and actions with non-local effects. Moreover, for a certain class of local-effect actions and knowledge bases for representing disjunctive information, we show that progression is not only fifirstorder defifinable but also effificiently computable