Paper Info
Title
On the Completeness of Propositional Hoare Logic
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.
Year
DOI
Venue
2001
10.1016/S0020-0255(01)00164-5
Information Sciences
Keywords
DocType
Volume
programs pi,expressiveness requirement,relationally valid rule,expressiveness assumption,propositional expressiveness condition,propositional hoare logic,propositional level,hoare logic,completeness result,computer science,technical report
Journal
139
Issue
ISSN
Citations 
3-4
0020-0255
11
PageRank 
References 
Authors
0.92
12
2
Name
Order
Citations
PageRank
Dexter C. Kozen15108912.56
Jerzy Tiuryn21210126.00