A hoare-style proof system for robot programs

Abstract

Golog is a situation calculus-based logic programming language for high-level robotic control. This paper ex-plores Hoare’s axiomatic approach to program verifica-tion in the Golog context. We present a novel Hoare-style proof system for partial correctness of Golog pro-grams. We prove total soundness of the proof system, and relative completeness of a subsystem of it for pro-cedureless Golog programs. Examples are given to il-lustrate the use of the proof system.