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

@inproceedings{vassos08conjecture, abstract = {In a seminal paper, Lin and Reiter introduced a model-theoretic 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 second-order 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 that the alternative definition is nonetheless correct for reasoning about a large class of sentences, including some that quantify over situations. In this case the alternative definition is a preferred option due to its simplicity and the fact that it is always first-order.}, author = {Vassos, Stavros and Levesque, Hector}, booktitle = {Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence (AAAI-08)}, citeulike-article-id = {3155120}, keywords = {ai, progression, reasoning\_about\_action, situation\_calculus}, location = {Chicago, Illinois, USA}, month = {July}, pages = {1004--1009}, posted-at = {2008-08-26 12:08:13}, priority = {0}, title = {On the Progression of Situation Calculus Basic Action Theories: Resolving a 10-year-old Conjecture}, url = {http://stavros.lostre.org/files/vassos08conjecture.pdf}, year = {2008} }

TY - CONF ID - vassos08conjecture L3 - citeulike-article-id:3155120 N2 - In a seminal paper, Lin and Reiter introduced a model-theoretic 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 second-order 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 that the alternative definition is nonetheless correct for reasoning about a large class of sentences, including some that quantify over situations. In this case the alternative definition is a preferred option due to its simplicity and the fact that it is always first-order. CY - Chicago, Illinois, USA EP - 1009 TI - On the Progression of Situation Calculus Basic Action Theories: Resolving a 10-year-old Conjecture T2 - Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence (AAAI-08) SP - 1004 KW - ai KW - progression KW - reasoning_about_action KW - situation_calculus AU - Vassos, Stavros AU - Levesque, Hector PY - 2008/07// UR - http://stavros.lostre.org/files/vassos08conjecture.pdf ER -