Foundations for Knowledge-Based Programs using ES.

Reiter proposed a semantics for knowledge-based Golog programs with sensing where program execution can be conditioned on tests involving explicit references to what the agent knows and does not know. An important result of this work is that reasoning about knowledge after the execution of actions can be reduced to classical reasoning from an initial first-order theory. However, it is limited in that tests can only refer to what is known about the current state, knowledge about knowledge is not considered, and the reduction does not apply to formulas with quantifying-in. This is in large part due to the choice of the underlying formalism, which is Reiter's version of the situation calculus. In this paper we show that, by moving to a new situation calculus recently proposed by Lakemeyer and Levesque, we cannot only reconstruct Reiter's foundations for knowledge-based programs but we can significantly go beyond them, which includes removing the above restrictions and more.