Accession Number:

ADA052443

Title:

A Proof-Checker for Dynamic Logic.

Descriptive Note:

Memorandum rept.,

Corporate Author:

MASSACHUSETTS INST OF TECH CAMBRIDGE ARTIFICIAL INTELLIGENCE LAB

Personal Author(s):

Report Date:

1977-06-01

Pagination or Media Count:

21.0

Abstract:

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 first-order logics of programs that manipulate their environment, including Floyds and Hoares logics of partial correctness and Manna and Waldingers 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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE