DROPS

Document

DOI: 10.4230/LIPIcs.LICS.2026.10

Hypersequent Calculi Have Ackermann Complexity

Authors: A. R. Balasubramanian, Vitor Greati, and Revantha Ramanayake

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on ℕ^d (Dickson’s lemma), yielding Ackermann upper bounds via controlled bad-sequence arguments. For hypersequent calculi, that argument lifted the ordering to the powerset, since a hypersequent is a (multi)set of sequents. This induces a jump from Ackermann to hyper-Ackermann complexity in the fast-growing hierarchy, suggesting that cut-free hypersequent calculi for extensions of the commutative Full Lambek calculus with contraction or weakening (FL_ec/FL_ew) inherently entail hyper-Ackermann upper bounds. We show that this intuition does not hold: every extension of FL_ec and FL_ew admitting a cut-free hypersequent calculus has an Ackermann upper bound on provability. To avoid the powerset, we exploit novel dependencies between individual sequents within any hypersequent in backward proof search. The weakening case, in particular, introduces a Karp-Miller-style acceleration, and it improves the upper bound for the fundamental fuzzy logic MTL. Our Ackermann upper bound is optimal for the contraction case (realized by the logic FL_ec).

Cite as

A. R. Balasubramanian, Vitor Greati, and Revantha Ramanayake. Hypersequent Calculi Have Ackermann Complexity. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 10:1-10:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{balasubramanian_et_al:LIPIcs.LICS.2026.10,
  author =	{Balasubramanian, A. R. and Greati, Vitor and Ramanayake, Revantha},
  title =	{{Hypersequent Calculi Have Ackermann Complexity}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{10:1--10:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.10},
  URN =		{urn:nbn:de:0030-drops-267970},
  doi =		{10.4230/LIPIcs.LICS.2026.10},
  annote =	{Keywords: Hypersequent calculi, Substructural logics, Ackermann complexity, Well-quasi-orders}
}

Document

DOI: 10.4230/LIPIcs.LICS.2026.46

The Logic of Bunched Implications Is Undecidable

Authors: Nikolaos Galatos, Peter Jipsen, Søren Brinck Knudstorp, and Revantha Ramanayake

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

The logic of bunched implications (BI), introduced by O’Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close connections to the propositional fragment of separation logic. We show here that provability in BI is undecidable by encoding Wang tilings into its ternary relational semantics. Equivalently, this yields the undecidability of the equational theory of BI-algebras. Our result is much more general, applying to the {∧, ∨, ¬, -*}-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then -* splits into two divisions ⧵, ∕). Consequently, our result covers an interval that includes BI, the non-commutative logic GBI, and Boolean BI (BBI), the latter already known to be undecidable. This result contrasts with a long-standing expectation that BI might be decidable. We also identify the gaps in the publications claiming decidability.

Cite as

Nikolaos Galatos, Peter Jipsen, Søren Brinck Knudstorp, and Revantha Ramanayake. The Logic of Bunched Implications Is Undecidable. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 46:1-46:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{galatos_et_al:LIPIcs.LICS.2026.46,
  author =	{Galatos, Nikolaos and Jipsen, Peter and Knudstorp, S{\o}ren Brinck and Ramanayake, Revantha},
  title =	{{The Logic of Bunched Implications Is Undecidable}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{46:1--46:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.46},
  URN =		{urn:nbn:de:0030-drops-268334},
  doi =		{10.4230/LIPIcs.LICS.2026.46},
  annote =	{Keywords: Bunched implication logic, Intuitionistic logic with operators, Residuated lattices, Substructural logics, Undecidable logics, Tiling problem}
}

Search Results

Documents authored by Ramanayake, Revantha

Hypersequent Calculi Have Ackermann Complexity

Abstract

Cite as

The Logic of Bunched Implications Is Undecidable

Abstract

Cite as

Thanks for your feedback!

Could not send message