论文标题
将kozen-tiuryn逻辑嵌入与测试的残留的一级kleene代数中
Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Tests
论文作者
论文摘要
Kozen和Tiuryn引入了子结构逻辑$ \ Mathsf {s} $，以推理程序的正确性（ACM TOCL，2003年）。逻辑$ \ mathsf {s} $区分了测试和部分正确性主张，以特殊的含义公式表示后者。 Kozen和Tiuryn的逻辑通过测试扩展了Kleene Altebra，其中部分正确性主张由方程式而不是术语表示。 Kleene代数与CODOMAIN，$ \ MATHSF {KAC} $，是Kleene代数的单分类替代方案，其测试可以通过操作员扩展Kleene代数，该操作员允许构建Boolean subalgebra测试的subalgebra。在本文中，我们表明，Kozen和Tiuryn的逻辑嵌入了$ \ Mathsf {kac} $扩展的方程理论中，并带有Kleene代数乘法的残留物以及代码量操作员的上部伴随。
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 between tests and partial correctness assertions, representing the latter by special implicational formulas. Kozen and Tiuryn's logic extends Kleene altebra with tests, where partial correctness assertions are represented by equations, not terms. Kleene algebra with codomain, $\mathsf{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 $\mathsf{KAC}$ with residuals of Kleene algebra multiplication and the upper adjoint of the codomain operator.
