A Proof-Checker for Dynamic Logic
Proceedings of the Fifth International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 552-557.
Abstract
We consider the problem of getting a computer to follow reasoning conducted in dynamic logic. This is a recently developed logic of programs that subsumes most existing firstorder logics of programs that manipulate their environment, including Floyd's and Hoare's logics of partial correctness and Manna and Waldinger's logic of total correctness. Dynamic . logic is more closely related to classical first-order logic than any other proposed logic of programs. This simplifies the design of a proof-checker for dynamic logic. Work in progress on the implementation of such a program is reported on, and an example machine-checked proof is exhibited.
@inproceedings{ijcai1977p126,
title = {A Proof-Checker for Dynamic Logic},
author = {Litvintchouk, Steven D. and Pratt, Vaughan R.},
booktitle = {Proceedings of the Fifth International Joint Conference on
Artificial Intelligence, {IJCAI-77}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Raj Reddy},
pages = {552--557},
year = {1977},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1977/126},
}
TY - CPAPER TI - A Proof-Checker for Dynamic Logic AU - Litvintchouk, Steven D. AU - Pratt, Vaughan R. T2 - Proceedings of the Fifth International Joint Conference on Artificial Intelligence, IJCAI-77 PB - International Joint Conferences on Artificial Intelligence PY - 1977 SP - 552 EP - 557 UR - https://ijcai.org/proceedings/1977/126 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
