Yilan Gu et al. [1]} 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 [2]}, 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.
