The situation calculus is a first-order language specifically designed for representing dynamically changing worlds. Agents can be modelled in the situation calculus by means of the Golog programming language, which provides macros for representing primitive actions, test actions, sequence, nondeterministic choice of two actions, nondeterministic choice of action arguments and nondeterministic iteration running on top of a Prolog interpreter.
The robot Charles and the Fantastic City is a metaphor used in the University of La Plata for teaching introductory courses to procedural programming. In this paper, we present an axiomatization of the robot Charles and the Fantastic City in the situation calculus as well as a controller written in Golog. A proof of the correctness of part of the proposed implementation is shown too.