The situation calculus: a case for modal logic.

*(English)*Zbl 1227.03022The paper starts with a reminder on Reiter’s situation calculus and basic action theories, illustrated with blocks-world examples. Knowledge can be expressed by introducing a special binary predicate \(K\) – the intended interpretation of \(K(s',s)\) being “situation \(s'\) is (epistemically) accessible from situation \(s\)”, which allows one to formalise knowledge of \(\phi\) in situation \(s\) as \(\forall s'.K(s',s)\supset\phi[s']\) –, not requesting that there be a unique initial situation, and adding a successor state axiom expressing that the situations which are accessible after doing an action are the successors of the situations which are accessible before doing the action and in which the action can be performed. Time can be modelled either by adding a new kind of individuals, or by making use of the implicit temporal structure of the tree of situations; both approaches are sketched, and the limitations emphasised, for instance, their inability to express that there is a path such that eventually \(\phi\) becomes true on this path. These considerations support the proposal for a modal language, less fine-grained in that it does not give access to situations, but expressive enough and allowing one to embed temporal aspects in a style similar to existing temporal logic.

In the second part of the paper, such a modal language, \(\mathcal{E\!S}\), is introduced. It contains formulas of the form Know\((\alpha)\), \(\square\alpha\) to express that “\(\alpha\) holds after any sequence of actions”, and \([t]\alpha\) to express that “\(\alpha\) holds after action \(t\)”. A classical Kripke semantics is presented. More precisely, defining an epistemic state as a subset of the set of worlds \(W\), and denoting by \(\mathcal Z\) the set of finite sequences of standard action names, the semantics determines whether or not \(e,w,z\models\phi\) holds for \(e\subseteq W\), \(w\in W\), and \(z\in\mathcal Z\). The key clauses are: \(e,w,z\models\text{Know}(\alpha)\) if \(e,w',z\models\alpha\) for all members \(w'\) of \(e\) that agree with \(w\) on the interpretation of all primitive rigid terms (a particular kind of terms); \(e,w,z\models\square\alpha\) if \(e,w,z\cdot z'\models\alpha\) for every \(z'\in\mathcal Z\); \(e,w,z\models[t]\alpha\) if \(e,w,z\cdot n\models\alpha\) where \(n\) is a standard name for the interpretation of \(t\) in \(w\). The usual properties of knowledge in weak S5 or K45 are proved to hold. It is shown with a one-line proof that if \(\alpha\) and \(\beta\) are formulas with no occurrence of Know and \(\models\alpha\supset\beta\), then \(\models\text{ Know}(\alpha)\supset\text{ Know}(\beta)\), a result which “in the original calculus, requires a complicated multi-page argument involving Craig’s interpolation lemma”.

Then the connection is made with Reiter’s situation calculus, thanks to a translation that maps the “situation-suppressed” formulas of \(\mathcal{E\!S}\) into formulas of that calculus. An appropriate set of axioms is introduced before the statement of the key “embedding theorem”, according to which for every basic sentence \(\alpha\) of \(\mathcal{E\!S}\) without standard names, \(\alpha\) is valid iff \(\alpha\)’s translation is a logical consequence of those axioms together with Reiter’s set of foundational axioms (it is observed that the latter can actually be replaced by a weaker set of axioms). In the last part of the paper, it is shown how to integrate branching time into \(\mathcal{E\!S}\), by introducing new modal operators, and in particular a path quantifier \(\mathbb E\). The semantics then determines whether or not \(e,w,z,\pi\models\phi\) holds for \(e\), \(w\) and \(z\) as before and \(\pi\) a path. In the extended language, one can formalise for instance that “there is a path such that whenever an object is on the table, then it will be on the floor some time after that” as

\[ \mathbb{E}(\forall x.\mathbb{G}(\text{OnTable}(x)\supset\mathbb{F}\text{OnFloor}(x))). \]

In the second part of the paper, such a modal language, \(\mathcal{E\!S}\), is introduced. It contains formulas of the form Know\((\alpha)\), \(\square\alpha\) to express that “\(\alpha\) holds after any sequence of actions”, and \([t]\alpha\) to express that “\(\alpha\) holds after action \(t\)”. A classical Kripke semantics is presented. More precisely, defining an epistemic state as a subset of the set of worlds \(W\), and denoting by \(\mathcal Z\) the set of finite sequences of standard action names, the semantics determines whether or not \(e,w,z\models\phi\) holds for \(e\subseteq W\), \(w\in W\), and \(z\in\mathcal Z\). The key clauses are: \(e,w,z\models\text{Know}(\alpha)\) if \(e,w',z\models\alpha\) for all members \(w'\) of \(e\) that agree with \(w\) on the interpretation of all primitive rigid terms (a particular kind of terms); \(e,w,z\models\square\alpha\) if \(e,w,z\cdot z'\models\alpha\) for every \(z'\in\mathcal Z\); \(e,w,z\models[t]\alpha\) if \(e,w,z\cdot n\models\alpha\) where \(n\) is a standard name for the interpretation of \(t\) in \(w\). The usual properties of knowledge in weak S5 or K45 are proved to hold. It is shown with a one-line proof that if \(\alpha\) and \(\beta\) are formulas with no occurrence of Know and \(\models\alpha\supset\beta\), then \(\models\text{ Know}(\alpha)\supset\text{ Know}(\beta)\), a result which “in the original calculus, requires a complicated multi-page argument involving Craig’s interpolation lemma”.

Then the connection is made with Reiter’s situation calculus, thanks to a translation that maps the “situation-suppressed” formulas of \(\mathcal{E\!S}\) into formulas of that calculus. An appropriate set of axioms is introduced before the statement of the key “embedding theorem”, according to which for every basic sentence \(\alpha\) of \(\mathcal{E\!S}\) without standard names, \(\alpha\) is valid iff \(\alpha\)’s translation is a logical consequence of those axioms together with Reiter’s set of foundational axioms (it is observed that the latter can actually be replaced by a weaker set of axioms). In the last part of the paper, it is shown how to integrate branching time into \(\mathcal{E\!S}\), by introducing new modal operators, and in particular a path quantifier \(\mathbb E\). The semantics then determines whether or not \(e,w,z,\pi\models\phi\) holds for \(e\), \(w\) and \(z\) as before and \(\pi\) a path. In the extended language, one can formalise for instance that “there is a path such that whenever an object is on the table, then it will be on the floor some time after that” as

\[ \mathbb{E}(\forall x.\mathbb{G}(\text{OnTable}(x)\supset\mathbb{F}\text{OnFloor}(x))). \]

Reviewer: Éric Martin (Sydney)

##### MSC:

03B42 | Logics of knowledge and belief (including belief change) |

68T27 | Logic in artificial intelligence |

PDF
BibTeX
Cite

\textit{G. Lakemeyer}, J. Logic Lang. Inf. 19, No. 4, 431--450 (2010; Zbl 1227.03022)

Full Text:
DOI

##### References:

[1] | Bacchus F., Kabanza F. (2000) Using temporal logics to express search control knowledge for planning. Artificial Intelligence 116(1–2): 123–191 · Zbl 0939.68827 |

[2] | Bacchus F., Halpern J.Y., Levesque H. (1999) Reasoning about noisy sensors and effectors in the situation calculus. Artificial Intelligence 111(1–2): 171–208 · Zbl 0996.68192 |

[3] | Baltag, A., Moss L. S., & Solecki, S. (1998). The logic of public announcements, common knowledge, and private suspicions. In Proceedings of the 7th conference on theoretical aspects of rationality and knowledge (TARK-VII) (pp. 43–56). · Zbl 1386.03019 |

[4] | Bienvenu, M., Fritz, Ch., & McIlraith, S. A. (2006). Planning with qualitative temporal preferences. In Proceedings of the tenth international conference on principles of knowledge representation and reasoning (KR’2004) (pp. 134–144). AAAI Press. |

[5] | Blackburn P., Kamps J., Marx M. (2001) Situation calculus as hybrid logic: First steps. In: Brazdil P., Jorge A. (eds) Progress in artificial intelligence. Lecture notes in artificial intelligence 2258. Springer, New York, pp 253–260 · Zbl 1053.68692 |

[6] | Boutilier, C., Reiter, R., Soutchanski, M., & Thrun, S. (2000). Decision-theoretic, high-level agent programming in the situation calculus. In Proceedings of AAAI-00 (pp. 355–362). AAAI Press. |

[7] | Burgard W., Cremers A.B., Fox D., Hähnel D., Lakemeyer G., Schulz D. et al (1999) Experiences with an interactive museum tour-guide robot. Artificial Intelligence 114(1–2): 3–55 · Zbl 0939.68865 |

[8] | Carbone, A., Finzi A., Orlandini, A., Pirri, F., & Ugazio, G. (2005). Augmenting situation awareness via model-based control in rescue robots. In Proceedings of IROS-2005. Edmonton, Canada. |

[9] | Castilho M. A., Gasquet O., Herzig A. (1999) Formalizing action and change in modal logic I: The frame problem. Journal of Logic and Computation 9(5): 701–735 · Zbl 0941.03021 |

[10] | Classen, J., & Lakemeyer, G. (2008). A logic for non-terminating Golog programs. In Proceedings of the eleventh conference on principles of knowledge representation and reasoning (KR 2008) (pp. 589–599). AAAI Press. |

[11] | Demolombe, R. (2003). Belief change: From Situation Calculus to Modal Logic. Journal of Applied Non-Classical Logics, 13(2). · Zbl 1185.03012 |

[12] | De Giacomo G., Lesperance Y., Levesque H. J. (2000) Congolog, a concurrent programming language based on the situation calculus. Artificial Intelligence 121: 109–169 · Zbl 0948.68175 |

[13] | Demolombe R., Herzig A., Varzinczak I. (2003) Regression in modal logic. Journal of Applied Non-Classical Logics 13(2): 165–185 · Zbl 1185.03028 |

[14] | Emerson E., Halpern J. Y. (1986) ”Sometimes” and ”not never” revisited: On branching versus linear time temporal logic. Journal of the ACM 33(1): 151–178 · Zbl 0629.68020 |

[15] | Fagin R., Halpern J., Moses Y., Vardi M. (1995) Reasoning about Knowledge. MIT Press, Cambridge, MA · Zbl 0839.68095 |

[16] | Ferrein A., Fritz C., Lakemeyer G. (2004) On-line decision-theoretic Golog for unpredictable domains. In: Biundo S., Frhwirt T., Palm G. (eds) KI2004: Advances in artificial intelligence. Springer, New York |

[17] | Fikes, R., & Nilsson, N. J. (1971). STRIPS: A new approach to the application of theorem proving to problem solving. In Proceedings of the second international joint conference on artificial intelligence (IJCAI-71) (pp. 608–620). · Zbl 0234.68036 |

[18] | Gabaldon, A. (2004). Precondition control and the progression algorithm. In Proceedings of the ninth international conference on principles of knowledge representation and reasoning (KR’2004) (pp. 634–664). AAAI Press. |

[19] | Grosskreutz H., Lakemeyer G. (2003) cc-Golog–An action language with continous change. Logic Journal of the IGPL 11(2): 179–221 · Zbl 1037.68144 |

[20] | Green, C. (1969). Application of theorem proving to problem solving. In Proceedings of the 1st international joint conference on artificial intelligence (IJCAI-69) (pp. 219–240). Washington, DC. |

[21] | Harel D. (1984) Dynamic logic. In: Gabbay D., Guenther F. (eds) Handbook of philosophical logic. D. Reidel, LK, pp 497–604 · Zbl 0875.03076 |

[22] | Herzig, A., Lang, J., Longin, D., & Polacsek, T. (2000). A logic for planning under partial observability. In Proceedings of AAAI-2000. AAAI Press. |

[23] | Hintikka J. (1962) Knowledge and belief. Cornell University Press, Ithaca · Zbl 1384.03102 |

[24] | Hughes G., Cresswell M. (1968) An introduction to modal logic. Methuen, London · Zbl 0205.00503 |

[25] | Kripke S. A. (1963) Semantical considerations on modal logic. Acta Philosophica Fennica 16: 83–94 · Zbl 0131.00602 |

[26] | Lakemeyer, G., & Levesque, H. J. (2004). Situations si, situation terms no. In Proceedings of the ninth international conference on principles of knowledge representation and reasoning (KR 2004) (pp. 516–526). AAAI Press. |

[27] | Lakemeyer, G., & Levesque, H. J. (2005). A useful fragment of the situation calculus. In Proceedings of the nineteenth international joint conference on artificial intelligence (IJCAI-05) (pp. 490–496). |

[28] | Lakemeyer, G., & Levesque, H. J. (2009). A semantic characterization of a useful fragment of the situation calculus with knowledge. In L. Morgenstern, V. Lifshitz & S. McIlraith (Eds.), Special issue in honor of John McCarthy, artificial intelligence. Elsevier (to appear). · Zbl 1216.68269 |

[29] | Levesque H. J., Lakemeyer G. (2001) The logic of knowledge bases. MIT Press, Cambridge, MA · Zbl 0998.68044 |

[30] | Levesque H. J., Lakemeyer G. (2008) Cognitive robotics. In: Harmelen F., Lifschitz V., Porter B. (eds) Handbook of knowledge representation. Elsevier, Amsterdam, pp 869–886 |

[31] | Levesque H. J., Reiter R., Lespérance Y., Lin F., Scherl R. B. (1997) Golog: A logic programming language for dynamic domains. Journal of Logic Programming 31: 59–84 · Zbl 0880.68008 |

[32] | Lutz, C. (2006). Complexity and succinctness of public announcement logic. In Proceedings of the fifth international joint conference on autonomous agents and multiagent systems (pp. 137–143). |

[33] | McCarthy, J. (1968). Situations, actions and causal laws. Technical report, Stanford University, 1963 [also in M. Minsky (Ed.), Semantic information processing (pp. 410–417). Cambridge, MA: MIT Press]. |

[34] | McIlraith, S., & Son, T. C. (2002). Adapting Golog for composition of semantic web services. In Proceedings of the eighth international conference on principles of knowledge representation and reasoning (pp. 482–493). San Francisco: Morgan Kaufmann. |

[35] | Moore R. C. (1985) A formal theory of knowledge and action. In: Hobbs J. R., Moore R. C. (eds) Formal theories of the commonsense world. Ablex, Norwood, NJ, pp 319–358 |

[36] | Pinto J. (1998) Integrating discrete and continuous change in a logical framework. Computational Intelligence 14(1): 39–88 |

[37] | Prior A. (1967) Past, present and future. Oxford University Press, Oxford · Zbl 0169.29802 |

[38] | Reiter, R. (1991). The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression. In V. Lifschitz (Ed.), Artificial intelligence and mathematical theory of computation (pp. 359–380). Academic Press. · Zbl 0755.68124 |

[39] | Reiter R. (2001a) Knowledge in action: Logical foundations for describing and implementing dynamical systems. MIT Press, Cambridge, MA · Zbl 1018.03022 |

[40] | Reiter, R. (2001b). On knowledge-based programming with sensing in the situation calculus. ACM Transactions on Computational Logic, 433–457. · Zbl 1365.68409 |

[41] | Scherl R. B., Levesque H. J. (2003) Knowledge, action, and the frame problem. Artificial Intelligence 144(1–2): 1–39 · Zbl 1079.68625 |

[42] | Shanahan M. (1997) Solving the frame problem: A mathematical investigation of the common sense law of inertia. MIT Press, Cambridge, MA |

[43] | van Benthem, J. (2009). Situation calculus meets modal logic. In L. Morgenstern, V. Lifshitz & S. McIlraith (Eds.), Special issue in honor of John McCarthy, artificial intelligence. Elsevier (to appear). |

[44] | van Ditmarsch, H., Herzig, A., & de Lima, T. (2007). Optimal regression for reasoning about knowledge and actions. In Proceedings of the twenty-second conference on artificial intelligence (AAAI-07) (pp. 1070–1075). |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.