REASONING FROM HYPOTHESES IN $\ast $-CONTINUOUS ACTION LATTICES

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