Implicational Kleene algebra with domain and the substructural logic of partial correctness
Igor Sedlár · Mathematical Structures in Computer Science · 2024
Abstract We show that Kozen and Tiuryn’s substructural logic of partial correctness $\mathsf{S}$ embeds into the equational theory of Kleene algebra with domain, $\mathsf{KAD}$ . We provide an implicational formulation of $\mathsf{KAD}$ which sets $\mathsf{S}$ in the context of implicational extensions of Kleene algebra.