On First-Order Definability and Computability of Progression for Local-Effect Actions and Beyond

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 first-order definable in general. Recently, Vassos,
Lakemeyer, and Levesque showed that in case
actions have only local effects, progression is firstorder
representable. However, they could show
computability of the first-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 first-order definable and computable. We
give a very simple proof for this via the concept
of forgetting. We also show first-order definability
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 firstorder
definable but also efficiently computable.