Representing and reasoning about program in situation calculus
Bo Yang, Mingyi Zhang, Maonian Wu, Gang Xie · Proceedings of SPIE, the International Society for Optical Engineering/Proceedings of SPIE · 2011
Situation calculus is an expressive tool for modeling dynamical system in artificial intelligence, changes in a dynamical world is represented naturally by the notions of action, situation and fluent in situation calculus. Program can be viewed as a discrete dynamical system, so it is possible to model program with situation calculus. To model program written in a smaller core programming language CL, notion of fluent is expanded for representing value of expression. Together with some functions returning concerned objects from expressions, a basic action theory of CL programming is constructed. Under such a theory, some properties of program, such as correctness and termination can be reasoned about.