A semantic characterization of a useful fragment of the situation calculus with knowledge Original Research Article

The situation calculus, as proposed by McCarthy and Hayes, and developed over the last decade by Reiter and co-workers, is reconsidered. A new logical variant called image is proposed that captures much of the expressive power of the original, but where certain technical results are much more easily proved. This is illustrated using two existing non-trivial results: the determinacy of knowledge theorem of Reiter and the regression theorem, which reduces reasoning about the future to reasoning about the initial situation. Furthermore, we show the correctness of our approach by embedding image in Reiterʹs situation calculus.