ML Anthology

A Hoare-Style Proof System for Robot Programs

Yongmei Liu
AAAI 2002 pp. 74-79
doi:10.5555/777092.777107 /aaai/2002/liu2002aaai-hoare/

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.

PDF AAAI Semantic Scholar

Cite

Text

Liu. "A Hoare-Style Proof System for Robot Programs." AAAI Conference on Artificial Intelligence, 2002. doi:10.5555/777092.777107

Markdown

[Liu. "A Hoare-Style Proof System for Robot Programs." AAAI Conference on Artificial Intelligence, 2002.](https://mlanthology.org/aaai/2002/liu2002aaai-hoare/) doi:10.5555/777092.777107

BibTeX

@inproceedings{liu2002aaai-hoare,
  title     = {{A Hoare-Style Proof System for Robot Programs}},
  author    = {Liu, Yongmei},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2002},
  pages     = {74-79},
  doi       = {10.5555/777092.777107},
  url       = {https://mlanthology.org/aaai/2002/liu2002aaai-hoare/}
}