Advertisement

Inductive definability and the situation calculus

  • Eugenia Ternovskaia
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1472)

Abstract

We explore the situation calculus within the framework of inductive definability. A consequence of this view of the situation calculus is to establish direct connections with different variants of the Μ-calculus [Par70,HP73,Pra81,Koz83,EC80], structural operational semantics of concurrent processes [Plo81], and logic programming [Apt90]. First we show that the induction principle on situations [Rei93] is implied by an inductive definition of the set of situations. Then we consider the frame problem from the point of view of inductive definability and by defining fluents inductively we obtain essentially the same form of successor state axioms as [Rei91]. Our approach allows extending this result to the case where ramification constraints are present. Finally we demonstrate a method of applying inductive definitions for computing fixed point properties of GOLOG programs.

Keywords

Logic Program Logic Programming Process Algebra Frame Problem Primitive Action 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Acz77]
    P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739–782. Elsevier, 1977.Google Scholar
  2. [Apt90]
    K. R. Apt. Logic programming. In Handbook of theoretical Computer Science, volume 92, pages 493–574. Elsevier, 1990.Google Scholar
  3. [BM77]
    J. Bell and M. Machover. A Course in Mathematical Logic. 1977.Google Scholar
  4. [BW90]
    J.C.M. Baeten and W.P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1990.Google Scholar
  5. [CC92]
    P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, pages 83–94, New York, U.S.A., 1992. ACM Press.Google Scholar
  6. [DGLL97]
    G. De Giacomo, H. J. Levesque, and Y. Lespérance. Reasoning about concurrent executions, prioritized interrupts, and exogenous actions in the situation calculus. In Proc. of IJCAI 97, pages 1221–1226, 1997.Google Scholar
  7. [DGTR97]
    G. De Giacomo, E. Ternovskaia, and R. Reiter. Non-terminating processes in the situation calculus. In Proc. of AAAI 97 workshop on Robots, Softbots, and Immobots: theories of action, planning and control, pages 18–28, 1997.Google Scholar
  8. [EC80]
    E. Emerson and E. Clarke. Characterizing correctness properties of parallel programs using fixpoints. volume 85 of Lecture Notes in Computer Science, pages 169–181. Springer Verlag, 1980.Google Scholar
  9. [Eme90]
    I.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 996–1072. ESP, 1990.Google Scholar
  10. [Heh93]
    E.C.R. Hehner. A practical theory of programming. Springer-Verlag, 1993.Google Scholar
  11. [HP73]
    P. Hitchcock and D. Park. Induction rules and termination proofs. In First Internat. Colloq. on Automata, Languages, and Programming, pages 225–251, North-Holland, Amsterdam, 1973.Google Scholar
  12. [Koz83]
    D. Kozen. Results on the prepositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.zbMATHMathSciNetCrossRefGoogle Scholar
  13. [Lei94]
    D. Leivant. Higher order logic. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, pages 229–321. Elsevier, 1994.Google Scholar
  14. [Lin95]
    F. Lin. Embracing causality in specifying the indirect effects of actions. In Proc. of IJCAI 95, pages 1985–1991, 1995.Google Scholar
  15. [LRL+96]
    H.J. Levesque, R. Reiter, Y. Lesperance, F. Lin, and R. Scherl. Golog: a logic programming language for dynamic domains. J. of Logic Programming, Special Issue on actions and processes, 4:655–678, 1996.Google Scholar
  16. [McI97]
    S.A. McIlraith. Representing actions and state constraints in model-based diagnosis. In Proc. of AAAI 97, pages 43–49, 1997.Google Scholar
  17. [Mil89]
    R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.Google Scholar
  18. [Mos74]
    Y.N. Moschovakis. Elementary Induction on Abstract Structures. Amsterdam, North Holland, 1974.Google Scholar
  19. [Par70]
    D. Park. Fixpoint induction and proofs of program properties. In Machine Intelligence, volume 5, pages 59–78. Edinburgh University Press, 1970.Google Scholar
  20. [Plo81]
    G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University,Denmark, 1981.Google Scholar
  21. [Pra81]
    V. Pratt. A decidable Μ-calculus (preliminary rept.). In Proc. 22th IEEE Symp. on Foundations of Computer Science, pages 421–427, 1981.Google Scholar
  22. [Rei91]
    R. Reiter. The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In Vladimir Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 359–380. Academic Press, San Diego, CA, 1991.Google Scholar
  23. [Rei93]
    R. Reiter. Proving properties of states in the situation calculus. J. of Artificial Intelligence, 64:337–351, 1993.zbMATHMathSciNetCrossRefGoogle Scholar
  24. [Thi96]
    M. Thielscher. Ramification and causality. Technical Report TR-96-003, International Computer Science Institute, Berkeley, CA 94704–1198, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Eugenia Ternovskaia
    • 1
  1. 1.Department of Computer ScienceUniversity of TorontoCanada

Personalised recommendations