Article

On Hoare Logic and Kleene Algebra with Tests

Author:

Dexter KozenAuthors Info & Claims

LICS '99: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science

Page 167

Published: 02 July 1999 Publication History

Publisher Site

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.

Cited By

View all

Mamouras K(2016)The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion SchemesACM Transactions on Computational Logic10.1145/283549117:2(1-30)Online publication date: 7-Jan-2016
https://dl.acm.org/doi/10.1145/2835491
Mamouras KHenzinger TMiller D(2014)On the Hoare theory of monadic recursion schemesProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603157(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603157
Schewe KThalheim B(2007)Term rewriting for web information systemsProceedings of the 8th international conference on Web information systems engineering10.5555/1781374.1781404(261-272)Online publication date: 3-Dec-2007
https://dl.acm.org/doi/10.5555/1781374.1781404
Show More Cited By

On Hoare Logic and Kleene Algebra with Tests

Recommendations

Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables
LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

This paper develops the correspondence between equality reasoning with axioms using λ-terms syntax, and reasoning using nominal terms syntax. Both syntaxes involve name-abstraction: λ-terms represent functional abstraction; nominal terms represent ...
On Hoare logic and Kleene algebra with tests

We show that Kleene algebra with tests (KAT) subsumes propositional Hoare logic (PHL). Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by simple equational reasoning. In addition, we show that all ...
On Hoare Logic and Kleene Algebra with Tests

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

LICS '99: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science

July 1999

ISBN:0769501583

Publisher

IEEE Computer Society

United States

Publication History

Published: 02 July 1999

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Mamouras K(2016)The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion SchemesACM Transactions on Computational Logic10.1145/283549117:2(1-30)Online publication date: 7-Jan-2016
https://dl.acm.org/doi/10.1145/2835491
Mamouras KHenzinger TMiller D(2014)On the Hoare theory of monadic recursion schemesProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603157(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603157
Schewe KThalheim B(2007)Term rewriting for web information systemsProceedings of the 8th international conference on Web information systems engineering10.5555/1781374.1781404(261-272)Online publication date: 3-Dec-2007
https://dl.acm.org/doi/10.5555/1781374.1781404
Schewe KThalheim B(2007)Personalisation of web information systems - A term rewriting approachData & Knowledge Engineering10.1016/j.datak.2006.07.00762:1(101-117)Online publication date: 1-Jul-2007
https://dl.acm.org/doi/10.1016/j.datak.2006.07.007
Chen HPucella R(2004)A coalgebraic approach to Kleene algebra with testsTheoretical Computer Science10.1016/j.tcs.2004.07.020327:1-2(23-44)Online publication date: 25-Oct-2004
https://dl.acm.org/doi/10.1016/j.tcs.2004.07.020

Abstract

Cited By

Recommendations

Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables