A Proof-Checker for Dynamic Logic.

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

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1977
Accession Number
ADA052443

Entities

People

  • S. D. Litvintchouk
  • V. R. Pratt

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Arithmetic
  • Artificial Intelligence
  • Automatic
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Language
  • Logic
  • Massachusetts
  • Military Research
  • Programming Languages
  • Reasoning
  • Software Development
  • Template Patterns
  • Verification

Fields of Study

  • Computer science

Readers

  • Computer Science.
  • Mathematical Modeling and Probability Theory.