A Hoare-Style Proof System for Robot Programs

Yongmei Liu, University of Toronto

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 Hoare-style 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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.