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:DagSemProc.10081.12, author = {Liu, Yongmei and Lakemeyer, Gerhard}, title = {{On First-Order Definability and Computability of Progression for Local-Effect Actions and Beyond}}, booktitle = {Cognitive Robotics}, pages = {1--7}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {10081}, editor = {Gerhard Lakemeyer and Hector J. Levesque and Fiora Pirri}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10081.12}, URN = {urn:nbn:de:0030-drops-26380}, doi = {10.4230/DagSemProc.10081.12}, annote = {Keywords: Action and change, knowledge representation} }
Feedback for Dagstuhl Publishing