Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. On the Completeness of Propositional Hoare Logic

On the Completeness of Propositional Hoare Logic

File(s)
99-1766.pdf (132 KB)
99-1766.ps (123.49 KB)
Permanent Link(s)
https://hdl.handle.net/1813/7420
Collections
Computer Science Technical Reports
Author
Kozen, Dexter
Tiuryn, Jerzy
Abstract

We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness result for Propositional Hoare Logic (PHL): all relationally valid rules {b1}p1{c1}, ..., {bn}pn{cn} --------------------------- {b}p{c} are derivable in PHL, provided the propositional expressiveness conditions are met. Moreover, if the programs pi in the premises are atomic, no expressiveness assumptions are needed.

Date Issued
1999-09
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR99-1766
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance