Situation calculus theory is used in the logical analysis of historical actions and transformations of agents that manipulate real-world objects. The situation calculus is germane in applications such as robotics, as well as temporal projection and planning [1], where domain knowledge experts define and use relevant axioms about the dynamics of each application to reason on the executed actions. In spite of the known branching structures of situations, how should we represent time and knowledge in a modal logic?
Lakemeyer critiques the inability of the situation calculus to adequately represent knowledge and time. He skillfully uses the actions of a robot in a block world to introduce the elements of the basic action theories and the projection problem. The groundwork axioms of the situation calculus contain an axiom that describes the set of all accessible situations from the initial situation by a chain of actions. To introduce knowledge into the situation calculus, Lakemeyer recommends replacing this axiom by an induction axiom to root all situations in some preliminary situation, adding a new axiom to make only the preliminary situations available at first, and ensuring that actions maintain the initial broad-spectrum property of the accessible situations.
Lakemeyer assesses the capability of the explicit time specification, and the use of the inherent chronological pattern of the tree of situations, to model time in the situation calculus. Consequently, he builds a first-order modal situation calculus, with branching time operators for coping with tree-like situations. The modal situation calculus consists of a unique language with symbols from a vocabulary, terms (the least set of expressions derived from actions and objects), and well-formed formulas of actions performed on objects at specific times.
The author presents clear, formal semantics for the modal situation calculus language. He convincingly illuminates the association of the modal situation calculus with Reiter’s well-known situational calculus. All modal logicians, as well as situation calculus skeptics, should read this insightful and engaging paper.