DocumentCode :
3037196
Title :
On Hoare logic and Kleene algebra with tests
Author :
Kozen, Dexter
Author_Institution :
Dept. of Comput. Sci., Cornell Univ., Ithaca, NY, USA
fYear :
1999
fDate :
1999
Firstpage :
167
Lastpage :
172
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 simple equational reasoning. We show using this reduction that propositional Hoare logic is PSPACE-complete
Keywords :
formal logic; Hoare logic; Kleene algebra; PSPACE-complete; equational reasoning; syntax; Algebra; Computer science; Dynamic programming; Encoding; Equations; Logic functions; Logic programming; Logic testing; Page description languages; Principal component analysis;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 1999. Proceedings. 14th Symposium on
Conference_Location :
Trento
ISSN :
1043-6871
Print_ISBN :
0-7695-0158-3
Type :
conf
DOI :
10.1109/LICS.1999.782610
Filename :
782610
Link To Document :
https://search.ricest.ac.ir/dl/search/defaultta.aspx?DTC=49&DC=3037196
بازگشت