Situation calculus has been widely applied in Artificial Intelligence related fields. This formalism is considered as a dialect of logic programming language and mostly used in dynamic domain modeling. However, type systems are hardly deployed in situation calculus in the literature. To achieve a correct and sound typed program written in situation calculus, adding typing elements into the current situation calculus will be quite helpful. In this paper, we propose to add more typing mechanisms to the current version of situation calculus, especially for three basic elements in situation calculus: situations, actions and objects, and then perform rigid type checking for existing situation calculus programs to find out the well-typed and ill-typed ones. In this way, type correctness and soundness in situation calculus programs can be guaranteed by type checking based on our type system. This modified version of a lightweight situation calculus is proved to be a robust and well-typed system.
Yilan @cite_3 proposed a modified version of the situation calculus built using a two-variable fragment of the first-order logic extended with counting quantifiers. By introducing several additional groups of axiom to capture taxonomic reasoning and using similar regression operator in Raymond Reiter's work @cite_4 , the projection and executability problems are proved decidable although an initial knowledge base is incomplete and open. While their system concerns primarily on semantics of the new components proposed but rarely talks about typing on them, our well-typed version of situation calculus mentions typing mechanisms together with a modified situation calculus version in an all around way.
@cite_4 @cite_3
2038809129 1825399774
Modeling and implementing dynamical systems is a central problem in artificial intelligence, robotics, software agents, simulation, decision and control theory, and many other disciplines. In recent years, a new approach to representing such systems, grounded in mathematical logic, has been developed within the AI knowledge-representation community. This book presents a comprehensive treatment of these ideas, basing its theoretical and implementation foundations on the situation calculus, a dialect of first-order logic. Within this framework, it develops many features of dynamical systems modeling, including time, processes, concurrency, exogenous events, reactivity, sensing and knowledge, probabilistic uncertainty, and decision theory. It also describes and implements a new family of high-level programming languages suitable for writing control programs for dynamical systems. Finally, it includes situation calculus specifications for a wide range of examples drawn from cognitive robotics, planning, simulation, databases, and decision theory, together with all the implementation code for these examples. This code is available on the book's Web site. We consider a modified version of the situation calculus built using a two-variable fragment of the first-order logic extended with counting quantifiers. We mention several additional groups of axioms that can be introduced to capture taxonomic reasoning. We show that the regression operator in this framework can be defined similarly to regression in the Reiter's version of the situation calculus. Using this new regression operator, we show that the projection and executability problems are decidable in the modified version even if an initial knowledge base is incomplete and open. For an incomplete knowledge base and for context-dependent actions, we consider a type of progression that is sound with respect to the classical progression. We show that the new knowledge base resulting after our progression is definable in our modified situation calculus if one allows actions with local effects only. We mention possible applications to formalization of Semantic Web services.