Reasoning from hypotheses in *-continuous action lattices

TL;DR

This paper investigates the complexity of reasoning in $ ext{ extasteriskcentered}$-continuous residuated Kleene lattices, revealing high computational complexity for general cases and lower complexity when only commutativity conditions are assumed.

Contribution

It extends the analysis of reasoning complexity from $ ext{ extasteriskcentered}$-continuous Kleene algebras to residuated lattices with residuals, providing new complexity bounds.

Findings

The Horn theory with $ ext{ extasteriskcentered}$-free hypotheses is hyperarithmetical.

Complexity reduces to $ ext{ extonequarter}^0_1$ when only commutativity is assumed.

Fragments are translated into infinitary action logic with exponentiation for upper bounds.

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.