Tower-Complete Problems in Contraction-Free Substructural Logics
| Autor: | Tanaka, Hiromi |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science computational complexity Theory of computation → Linear logic Mathematics - Logic deducibility full Lambek calculus Logic in Computer Science (cs.LO) Theory of computation → Proof theory substructural logic linear logic FOS: Mathematics BCK-logic provability Theory of computation → Complexity theory and logic Logic (math.LO) |
| DOI: | 10.4230/lipics.csl.2023.34 |
| Popis: | We investigate the non-elementary computational complexity of a family of substructural logics without contraction. With the aid of the technique pioneered by Lazi\'c and Schmitz (2015), we show that the deducibility problem for full Lambek calculus with exchange and weakening ($\mathbf{FL}_{\mathbf{ew}}$) is not in Elementary (i.e., the class of decision problems that can be decided in time bounded by an elementary recursive function), but is in PR (i.e., the class of decision problems that can be decided in time bounded by a primitive recursive function). More precisely, we show that this problem is complete for Tower, which is a non-elementary complexity class forming a part of the fast-growing complexity hierarchy introduced by Schmitz (2016). The same complexity result holds even for deducibility in BCK-logic, i.e., the implicational fragment of $\mathbf{FL}_{\mathbf{ew}}$. We furthermore show the Tower-completeness of the provability problem for elementary affine logic, which was proved to be decidable by Dal Lago and Martini (2004). Comment: The full version of the paper accepted to CSL 2023 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|