Some contributions to the metatheory of the situation calculus

ABSTRACT

We focus on a rich axiomatization for actions in the situation calculus that includes, among other features, a solution to the frame problem for deterministic actions. Our work is foundational in nature, directed at simplifying the entailment problem for these axioms. Specifically, we make four contributions to the metatheory of situation calculus axiomatizations of dynamical systems: (1) We prove that the above-mentioned axiomatization for actions has a relative satisfiability property; the full axiomatization is satisfiable iff the axioms for the initial state are. (2)We define the concept of regression relative to these axioms, and prove a soundness and completeness theorem for a regression-based approach to the entailment problem for a wide class of queries. (3) Our formalization of the situation calculus requires certain foundational axioms specifying the domain of situations. These include an induction axiom, whose presence complicates human and automated reasoning in the situation calculus. We characterize various classes of sentences whose proofs do not require induction, and in some cases, some of the other foundational axioms. (4)We prove that the logic programming language GOLOG never requires any of the foundational axioms for the evaluation of programs.

REFERENCES

• 1: James F. Allen, Towards a general theory of action and time, Artificial Intelligence, v.23 n.2, p.123-154, July 1984 [doi>10.1016/0004-3702(84)90008-0]
• 2: Leopoldo Bertossi , Marcelo Arenas , Cristian Ferretti, SCDBR: An Automated Reasoner for Specifications of Database Updates, Journal of Intelligent Information Systems, v.10 n.3, p.253-280, June 1, 1998 [doi>10.1023/A:1013861118705]
• 3: Wolfram Burgard , Armin B. Cremers , Dieter Fox , Dirk Hähnel , Gerhard Lakemeyer , Dirk Schulz , Walter Steiner , Sebastian Thrun, The interactive museum tour-guide robot, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.11-18, July 1998, Madison, Wisconsin, United States
• 4: Ernest Davis, Representations of commonsense knowledge, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1990
• 5: DE GIACOMO, G., LESPERANCE, Y., AND LEVESQUE, U. J. 1997. Reasoning about concurrent execution, prioritized interrupts, and exogenous actions in the situation calculus. In Proceedings of the 14th International Joint Conference on Artificial Intelligence (Nagoya, Japan). pp. 1221-1226.
• 6: ENDERTON, H.B. 1972. A Mathematical Introduction to Logic. Academic Press, Orlando, Fla.
• 7: John David Funge, Making them behave: cognitive models for computer animation, University of Toronto, Toronto, Ont., Canada, 1998
• 8: GELFOND, M., AND LIFSCHITZ, V. 1998. Action languages. Linkdping Electronic Articles in Computer and Information Sciences, 3, www.ep.liu.se/ea/cis/1998/016/.
• 9: GELFOND, M., LIFSCHITZ, V., AND RABINOV, A. 1991. What are the limitations of the situation calculus? In Working Notes, AAAI Spring Symposium Series on the Logical Formalization of Commonsense Reasoning. AAAI Press, Reston, Va., pp. 50-69.
• 10: Robert Goldblatt, Logics of time and computation, Center for the Study of Language and Information, Stanford, CA, 1987
• 11: GALEN, C.C. 1969. Theorem proving by resolution as a basis for question-answering systems. In Machine Intelligence, vol. 4, B. Meltzer and D. Mitchie, eds. American Elsevier, New York, pp. 183-205.
• 12: HAAS, A.R. 1987. The case for domain-specific frame axioms. In The Frame Problem in Artificial Intelligence. Proceedings of the 1987 Workshop, Los Altos, Calif., F. M. Brown, ed. Morgan- Kaufmann, San Francisco, Calif., pp. 343-348.
• 13: HANKS, S., AND MCDERMOTT, D. 1986. Default reasoning, nonmonotonic logics, and the frame problem. In Proceedings of the National Conference on Artificial Intelligence (AAAI'86). AAAI Press, Reston, Va., pp. 328-333.
• 14: JENKIN, M., LESPt#RANCE, Y., LEVESQUE, H. J., LIN, F., LLOYD, J., MARCU, D., REITER, R., SCHERL, R. B., AND TAM, K. 1997. A logical approach to portable high-level robot programming (Invited paper). In Proceedings of the lOth Australian Joint Conference on Artificial Intelligence (/t1'97) (Perth, Australia).
• 15: R Kowalski , M Sergot, A logic-based calculus of events, New Generation Computing, v.4 n.1, p.67-95, 1986 [doi>10.1007/BF03037383]
• 16: LESPt#RANCE, Y., LEVESQUE, H. J., AND REITER, R. 1997. A situation calculus approach to modeling and programming agents. In Foundations and Theories of Rational Agency, A. Rao and M. Wooldridge, eds. in press.
• 17: LEVESQUE, H.J. 1996. What is planning in the presence of sensing? In Proceedings of the National Conference on Artificial Intelligence (AAAI'96). AAAI Press, Reston, Va., pp. 1139-1146.
• 18: LEVESQUE, H. J., REITER, R., LESPt#RANCE, Y., LIN, F., AND SCHERL, R. 1997. GOLOG: A logic programming language for dynamic domains. J. Logic Prog. Special Issue on Actions, 31, 1-3, 59-83.
• 19: LIFSCHITZ, V. 1991. Toward a metatheory of action. In Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR'91) (Los Altos, Calif.). J. Allen, R. Fikes, and E. Sandewall, eds. Morgan-Kaufmann, San Francisco, Calif., pp. 376-386.
• 20: LIN, F., AND REITER, R. 1994. State constraints revisited. J. Logic Comput. Special Issue on Actions and Processes, 4, 655-678.
• 21: Fangzhen Lin , Ray Reiter, How to progress a database, Artificial Intelligence, v.92 n.1-2, p.131-167, May 1997 [doi>10.1016/S0004-3702(96)00044-6]
• 22: MCCARTHY, J. 1968. Situations, actions and causal laws. In Semantic Information Processing, M. Minsky ed. HIT Press, Cambridge, Mass., pp. 410-417.
• 23: MCCARTHY, J. 1977. Epistemological problems of artificial intelligence. In Proceedings of the 5th International Joint Conference on Artificial Intelligence (Cambridge, Mass.). pp. 1038-1044.
• 24: Drew McDermott, Nonmonotonic Logic II: Nonmonotonic Modal Theories, Journal of the ACM (JACM), v.29 n.1, p.33-57, Jan. 1982 [doi>10.1145/322290.322293]
• 25: Sheila Ann Mcilraith , Raymond Reiter, Towards a formal account of diagnostic problem-solving, 1997
• 26: E. P. D. Pednault, Toward a mathematical theory of plan synthesis, Stanford University, Stanford, CA, 1987
• 27: Edwin P. D. Pednault, ADL: exploring the middle ground between STRIPS and the situation calculus, Proceedings of the first international conference on Principles of knowledge representation and reasoning, p.324-332, December 1989
• 28: Javier Andres Pinto , Raymond Reiter, Temporal reasoning in the situation calculus, 1994
• 29: PINTO, J. 1999. Occurrences and narratives as constraints in the branching structure of the situation calculus. J. Logic Comput., to appear, URL = ftp://lyrcc.ing.puc.cl/pub/jpinto/jlc.ps.gz.
• 30: REITER, R. 1999. Knowledge in action: Logical foundations for describing and implementing dynamical systems. In preparation. Draft available at http://www.cs.toronto.edu/#cogrobo/.
• 31: Raymond Reiter, The frame problem in situation the calculus: a simple solution (sometimes) and a completeness result for goal regression, Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, Academic Press Professional, Inc., San Diego, CA, 1991
• 32: Raymond Reiter, Proving properties of states in the situation calculus, Artificial Intelligence, v.64 n.2, p.337-351, Dec. 1993 [doi>10.1016/0004-3702(93)90109-O]
• 33: REITER, R. 1995. On specifying database updates. J. Logic Prog. 25, 25-91.
• 34: REITER, R. 1996. Natural actions, concurrency and continuous time in the situation calculus. In Principles of Knowledge Representation and Reasoning: Proceedings of the 5th International Conference (KR'96). L. C. Aiello, J. Doyle, and S. C. Shapiro, eds. Morgan-Kaufmann, San Francisco, Calif., pp. 2-13.
• 35: REITER, R. 1998. Sequential, temporal GOLOG. In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR'98). A. C. Cohn and L. K. Schubert, eds. Morgan-Kaufmann, San Francisco, Calif., pp. 547-556.
• 36: Erik Sandewall, Features and fluents (vol. 1): the representation of knowledge about dynamical systems, Oxford University Press, Inc., New York, NY, 1995
• 37: SCHUBEaT, L. K. 1990. Monotonic solution of the frame problem in the situation calculus: An efficient method for worlds with fully specified actions. In Knowledge Representation and Defeasible Reasoning. H. E. Kyberg, R. P. Loui, and G. N. Carlson, eds. Kluwer Academic Press. pp. 23-67.
• 38: Murray Shanahan, Solving the frame problem: a mathematical investigation of the common sense law of inertia, MIT Press, Cambridge, MA, 1997
• 39: STOY, J.E. 1977. Denotational Semantics. MIT Press, Cambridge, Mass.
• 40: WALDINGER, R. 1977. Achieving several goals simultaneously. In Machine Intelligence 8. E. Elcock and D. Michie, eds. Ellis Horwood, Edinburgh, Scotland, pp. 94-136.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

General Terms:
Theory

Keywords:
programming languages for the situation calculus, regression, situation calculus, theorem-proving