Proceedings:
Book One
Volume
Issue:
Proceedings of the AAAI Conference on Artificial Intelligence, 18
Track:
Knowledge Representation
Downloads:
Abstract:
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.
AAAI
Proceedings of the AAAI Conference on Artificial Intelligence, 18