Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Test
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F22%3A00565990" target="_blank" >RIV/67985807:_____/22:00565990 - isvavai.cz</a>
Result on the web
<a href="https://dx.doi.org/10.1007/978-3-031-15298-6_14" target="_blank" >https://dx.doi.org/10.1007/978-3-031-15298-6_14</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-15298-6_14" target="_blank" >10.1007/978-3-031-15298-6_14</a>
Alternative languages
Result language
angličtina
Original language name
Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Test
Original language description
Kozen and Tiuryn have introduced the substructural logic S for reasoning about correctness of while programs (ACM TOCL, 2003). The logic S distinguishes between tests and partial correctness assertions, representing the latter by special implicational formulas. Kozen and Tiuryn's logic extends Kleene algebra with tests, where partial correctness assertions are represented by equations, not terms. Kleene algebra with codomain, KAC, is a one-sorted alternative to Kleene algebra with tests that expands Kleene algebra with an operator that allows to construct a Boolean subalgebra of tests. In this paper we show that Kozen and Tiuryn's logic embeds into the equational theory of the expansion of KAC with residuals of Kleene algebra multiplication and the upper adjoint of the codomain operator.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/EF18_053%2F0017594" target="_blank" >EF18_053/0017594: Supporting the internationalization of the Institute of Computer Science of the Czech Academy of Sciences</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Logic, Language, Information, and Computation
ISBN
978-3-031-15297-9
ISSN
0302-9743
e-ISSN
—
Number of pages
16
Pages from-to
221-236
Publisher name
Springer
Place of publication
Cham
Event location
Iași
Event date
Sep 20, 2022
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000866553800014