Due to its powerful action-based reasoning ability, situation calculus is often chosen as the formalism to express other models and programming languages which are either too complex to understand and use, like Artificial Intelligence in games [1]} and Planning Domain Definition Language (PDDL) [2]}, or a little powerless to represent an entire complicated systems of different types, like Action Description Language (ADL) [3]}. In the literature employing situation calculus as a formal method to express the semantics in PDDL [4]} and ADL [5]}, the authors have tried to introduce some typing mechanisms, which is only limited to add type element in syntax, and only applied to variables. Other significant terms, such as fluents and predicates, are still typeless. Moreover, in semantics and reasoning, typing mechanisms are hardly discussed in these papers, neither is type checking.
