The class of all $\ast $-continuous Kleene algebras, whose description includes an infinitary condition on the iteration operator, plays an important role in computer science. The complexity of reasoning in such algebras—ranging from the equational theory to the Horn one, with restricted fragments of the latter in between—was analyzed by Kozen (2002). This paper deals with similar problems for $\ast $-continuous residuated Kleene lattices, also called $\ast $-continuous action lattices, where the product operation is augmented by residuals. We prove that, in the presence of residuals, the fragment of the corresponding Horn theory with $\ast $-free hypotheses has the same complexity as the $\omega ^\omega $ iteration of the halting problem, and hence is properly hyperarithmetical. We also prove that if only commutativity conditions are allowed as hypotheses, then the complexity drops down to $\Pi ^0_1$ (i.e., the complement of the halting problem), which is the same as that for $\ast $-continuous Kleene algebras. In fact, we get stronger upper bound results: the fragments under consideration are translated into suitable fragments of infinitary action logic with exponentiation, and our upper bounds are obtained for the latter ones.

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.

We show that any regular pseudocomplemented Kleene algebra defined on an algebraic lattice is isomorphic to a rough set Kleene algebra determined by a tolerance induced by an irredundant covering.

Consider the quasi-variety generated by a finite algebra and assume that yields a natural duality on based on which is optimal modulo endomorphisms. We shoe that, provided satisfies certain minimality conditions, we can transfer this duality to a natural duality on based on , which is also optimal modulo endormorphisms, for any finite algebra in that has a subalgebra isomorphic to .