Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Test

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Test

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Test

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/EF18_053%2F0017594" target="_blank" >EF18_053/0017594: Podpora internacionalizace Ústavu informatiky AV ČR, v.v.i</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Logic, Language, Information, and Computation

ISBN

978-3-031-15297-9

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

16

Strana od-do

221-236

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Iași

Datum konání akce

20. 9. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000866553800014