A Hoare-Style Proof System for Robot Programs

Golog is a situation calculus-based logic programming language for high-level robotic control. This paper explores Hoare’s axiomatic approach to program verification in the Golog context. We present a novel Hoarestyle proof system for partial correctness of Golog programs. We prove total soundness of the proof system, and relative completeness of a subsystem of it for procedureless Golog programs. Examples are given to illustrate the use of the proof system.

Authors

• Yongmei Liu SUN YAT-SEN UNIVERSITY

Keywords

No keywords are indexed for this paper.