# Inductive definability and the situation calculus

## 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## Preview

Unable to display preview. Download preview PDF.

## References

- [Acz77]P. Aczel. An introduction to inductive definitions. In J. Barwise, editor,
*Handbook of Mathematical Logic*, pages 739–782. Elsevier, 1977.Google Scholar - [Apt90]K. R. Apt. Logic programming. In
*Handbook of theoretical Computer Science*, volume 92, pages 493–574. Elsevier, 1990.Google Scholar - [BM77]J. Bell and M. Machover.
*A Course in Mathematical Logic*. 1977.Google Scholar - [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 - [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 - [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 - [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 - [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 - [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 - [Heh93]E.C.R. Hehner.
*A practical theory of programming*. Springer-Verlag, 1993.Google Scholar - [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 - [Koz83]D. Kozen. Results on the prepositional mu-calculus.
*Theoretical Computer Science*, 27:333–354, 1983.zbMATHMathSciNetCrossRefGoogle Scholar - [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 - [Lin95]F. Lin. Embracing causality in specifying the indirect effects of actions. In
*Proc. of IJCAI 95*, pages 1985–1991, 1995.Google Scholar - [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 - [McI97]S.A. McIlraith. Representing actions and state constraints in model-based diagnosis. In
*Proc. of AAAI 97*, pages 43–49, 1997.Google Scholar - [Mil89]R. Milner.
*Communication and Concurrency*. Prentice-Hall International, Englewood Cliffs, 1989.Google Scholar - [Mos74]Y.N. Moschovakis.
*Elementary Induction on Abstract Structures*. Amsterdam, North Holland, 1974.Google Scholar - [Par70]D. Park. Fixpoint induction and proofs of program properties. In
*Machine Intelligence*, volume 5, pages 59–78. Edinburgh University Press, 1970.Google Scholar - [Plo81]G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University,Denmark, 1981.Google Scholar
- [Pra81]V. Pratt. A decidable
*Μ*-calculus (preliminary rept.). In*Proc. 22th IEEE Symp. on Foundations of Computer Science*, pages 421–427, 1981.Google Scholar - [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 - [Rei93]R. Reiter. Proving properties of states in the situation calculus.
*J. of Artificial Intelligence*, 64:337–351, 1993.zbMATHMathSciNetCrossRefGoogle Scholar - [Thi96]M. Thielscher. Ramification and causality. Technical Report TR-96-003, International Computer Science Institute, Berkeley, CA 94704–1198, 1996.Google Scholar