Hoare logic for GOLOG programs

grantor: University of TorontoGOLOG is a situation calculus-based logic programming language for dynamic domains like robots, industrial processes, intelligent software agents, etc. This thesis explores Hoare's axiomatic approach to program verification in the GOLOG context. We present Hoare-style proof systems for partial correctness and termination of procedure-less GOLOG programs, and prove the corresponding soundness and completeness results. We extend these proof systems to deal with partial correctness and termination of recursive GOLOG procedures, and prove the soundness of the resulting systems. Examples are given to illustrate the use of these proof systems.M.Sc