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

Igor Sedlár, Johann J. Wannenburg

Kozen and Tiuryn have introduced the substructural logic $\mathsf{S}$ for reasoning about correctness of while programs (ACM TOCL, 2003). The logic $\mathsf{S}$ distinguishes betwe…