Skip to main content


eCommons@Cornell

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

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/7377
Title: On Hoare Logic and Kleene Algebra with Tests
Authors: Kozen, Dexter
Keywords: computer science
technical report
Issue Date: Dec-1998
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR98-1723
Abstract: We show that Kleene algebra with tests subsumes propositional Hoare logic. Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by ordinary equational reasoning. It follows from the reduction that propositional Hoare logic is in PSPACE; we show that it is PSPACE-complete.
URI: http://hdl.handle.net/1813/7377
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
98-1723.pdf223.75 kBAdobe PDFView/Open
98-1723.ps551.15 kBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us