Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2408.02118 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912233930358784 |
|---|---|
| author | Kuznetsov, Stepan L. Pshenitsyn, Tikhon Speranski, Stanislav O. |
| author_facet | Kuznetsov, Stepan L. Pshenitsyn, Tikhon Speranski, Stanislav O. |
| contents | 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 $ω^ω$ 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 $Π^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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_02118 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Reasoning from hypotheses in *-continuous action lattices Kuznetsov, Stepan L. Pshenitsyn, Tikhon Speranski, Stanislav O. Logic 03B47 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 $ω^ω$ 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 $Π^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. |
| title | Reasoning from hypotheses in *-continuous action lattices |
| topic | Logic 03B47 |
| url | https://arxiv.org/abs/2408.02118 |