Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: On the Completeness of Propositional Hoare Logic
Authors: Kozen, Dexter
Tiuryn, Jerzy
Keywords: computer science
technical report
Issue Date: Sep-1999
Publisher: Cornell University
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.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
99-1766.pdf132 kBAdobe PDFView/Open
99-1766.ps123.49 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us