On the Progression of Situation Calculus Basic Action Theories: Resolving a 10-year-old Conjecture

In a seminal paper, Lin and Reiter introduced a modeltheoretic definition for the progression of the initial knowledge base of a basic action theory. This definition comes with a strong negative result, namely that for certain kinds of action theories, first-order logic is not expressive enough to correctly characterize this form of progression, and secondorder axioms are necessary. However, Lin and Reiter also considered an alternative definition for progression which is always first-order definable. They conjectured that this alternative definition is incorrect in the sense that the progressed theory is too weak and may sometimes lose information. This conjecture, and the status of first-order definable progression, has remained open since then. In this paper we present two significant results about this alternative definition of progression. First, we prove the Lin and Reiter conjecture by presenting a case where the progressed theory indeed does lose information. Second, we prove ...

• Type: Conference
• Year: 2008
• Where: AAAI
• Authors: Stavros Vassos, Hector J. Levesque
• Keywords: AAAI 2008, Alternative Definition, First-order Definable Progression, Intelligent Agents, Reiter