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.

@InProceedings{liu_et_al:DSP:2010:2638,
  author =	{Yongmei Liu and Gerhard Lakemeyer},
  title =	{On First-Order Definability and Computability of Progression for Local-Effect Actions and Beyond},
  booktitle =	{Cognitive Robotics},
  year =	{2010},
  editor =	{Gerhard Lakemeyer and Hector J. Levesque and Fiora Pirri},
  number =	{10081},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2638},
  annote =	{Keywords: Action and change, knowledge representation}
}