License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2023.34
URN: urn:nbn:de:0030-drops-174954
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17495/
Go to the corresponding LIPIcs Volume Portal

Tanaka, Hiromi

Tower-Complete Problems in Contraction-Free Substructural Logics

pdf-format:
LIPIcs-CSL-2023-34.pdf (1.0 MB)

Abstract

We investigate the non-elementary computational complexity of a family of substructural logics without contraction. With the aid of the technique pioneered by Lazić and Schmitz (2015), we show that the deducibility problem for full Lambek calculus with exchange and weakening (FL_{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 FL_{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).

BibTeX - Entry

@InProceedings{tanaka:LIPIcs.CSL.2023.34,
  author =	{Tanaka, Hiromi},
  title =	{{Tower-Complete Problems in Contraction-Free Substructural Logics}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{34:1--34:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17495},
  URN =		{urn:nbn:de:0030-drops-174954},
  doi =		{10.4230/LIPIcs.CSL.2023.34},
  annote =	{Keywords: substructural logic, linear logic, full Lambek calculus, BCK-logic, computational complexity, provability, deducibility}
}

Keywords: substructural logic, linear logic, full Lambek calculus, BCK-logic, computational complexity, provability, deducibility
Collection: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Issue Date: 2023
Date of publication: 01.02.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI