Document Open Access Logo

Hypersequent Calculi Have Ackermann Complexity

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.10.pdf
  • Filesize: 1.07 MB
  • 26 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Linear logic
Keywords
  • Hypersequent calculi
  • Substructural logics
  • Ackermann complexity
  • Well-quasi-orders

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.LICS.2026.10

Author Details

A. R. Balasubramanian
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Vitor Greati
  • Bernoulli Institute, University of Groningen, The Netherlands
Revantha Ramanayake
  • Bernoulli Institute, University of Groningen, The Netherlands

Funding

  • Balasubramanian, A. R.: This research was sponsored in part by the Deutsche Forschungsgemeinschaft project https://gepris.dfg.de/gepris/projekt/389792660 TRR 248–CPEC.
  • Ramanayake, Revantha: Supported by Dutch Research Council (NWO) project OCENW.M.22.258.

References

  1. A. Avron. A constructive analysis of RM. J. of Symbolic Logic, 52(4):939-951, 1987. URL: https://doi.org/10.2307/2273828.
  2. A. R. Balasubramanian. Complexity of controlled bad sequences over finite sets of ℕ^d. In ACM International Conference Proceeding Series, pages 130-140. Association for Computing Machinery, July 2020. URL: https://doi.org/10.1145/3373718.3394753.
  3. A. R. Balasubramanian, Vitor Greati, and Revantha Ramanayake. Hypersequent calculi have Ackermannian complexity, 2026. URL: https://doi.org/10.48550/arXiv.2602.19229.
  4. A. R. Balasubramanian, Timo Lang, and Revantha Ramanayake. Decidability and complexity in weakening and contraction hypersequent substructural logics. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470733.
  5. P. Baldi, A. Ciabattoni, and L. Spendier. Standard completeness for extensions of MTL: an automated approach. In WOLLIC 2012, volume 7456 of LNCS, pages 154-167. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32621-9_12.
  6. Sébastien Bardin, Alain Finkel, Jérôme Leroux, and Laure Petrucci. FAST: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf., 10(5):401-424, 2008. URL: https://doi.org/10.1007/S10009-008-0064-3.
  7. A. Ciabattoni, N. Galatos, and K. Terui. From axioms to analytic rules in nonclassical logics. In LICS 2008, pages 229-240, 2008. URL: https://doi.org/10.1109/LICS.2008.39.
  8. Agata Ciabattoni, Francesc Esteva, and Lluıs Godo. T-norm based logics with n-contraction. Neural Network World, 12:441-452, January 2002. Google Scholar
  9. Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. Algebraic proof theory: Hypersequents and hypercompletions. Ann. Pure Appl. Logic, 168(3):693-737, 2017. URL: https://doi.org/10.1016/j.apal.2016.10.012.
  10. Peter Clote. Computational models and function algebras. In Daniel Leivant, editor, Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, International Workshop LCC '94, Indianapolis, Indiana, USA, 13-16 October 1994, volume 960 of Lecture Notes in Computer Science, pages 98-130. Springer, 1994. URL: https://doi.org/10.1007/3-540-60178-3_81.
  11. Leonard Eugene Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics, 35(4):413-422, 1913. Google Scholar
  12. Francesc Esteva and Lluıs Godo. Monoidal t-norm based logic: towards a logic for left-continuous t-norms. Fuzzy Sets and Systems, 124(3):271-288, 2001. Fuzzy Logic. URL: https://doi.org/10.1016/S0165-0114(01)00098-7.
  13. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s lemma. In Proceedings - Symposium on Logic in Computer Science, pages 269-278, 2011. URL: https://doi.org/10.1109/LICS.2011.39.
  14. N. Galatos, P. Jipsen, T. Kowalski, and H. Ono. Residuated lattices: an algebraic glimpse at substructural logics, volume 151 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2007. Google Scholar
  15. Zuzana Haniková. Complexity of some language fragments of fuzzy logics. Soft Computing, 21(1):69-77, 2017. URL: https://doi.org/10.1007/s00500-016-2346-0.
  16. Rostislav Horcík, Carles Noguera, and Milan Petrık. On n-contractive fuzzy logics. Mathematical Logic Quarterly, 53:268-288, June 2007. URL: https://doi.org/10.1002/malq.200610044.
  17. Rostislav Horčík and Kazushige Terui. Disjunction property and complexity of substructural logics. Theoretical Computer Science, 412(31):3992-4006, 2011. URL: https://doi.org/10.1016/j.tcs.2011.04.004.
  18. Emil Jerábek. A note on the substructural hierarchy. Math. Log. Q., 62(1-2):102-110, 2016. URL: https://doi.org/10.1002/MALQ.201500066.
  19. Richard M. Karp and Raymond E. Miller. Parallel program schemata. J. Comput. Syst. Sci., 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  20. S. Kripke. The problem of entailment (abstract). J. of Symbolic Logic, 24:324, 1959. Google Scholar
  21. Ranko Lazic and Sylvain Schmitz. The complexity of coverability in ν-petri nets. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 467-476. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933593.
  22. Ranko Lazic and Sylvain Schmitz. The ideal view on Rackoff’s coverability technique. Inf. Comput., 277:104582, 2021. URL: https://doi.org/10.1016/J.IC.2020.104582.
  23. Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere! In Doron A. Peled and Yih-Kuen Tsay, editors, Automated Technology for Verification and Analysis, Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings, volume 3707 of Lecture Notes in Computer Science, pages 489-503. Springer, 2005. URL: https://doi.org/10.1007/11562948_36.
  24. George Metcalfe, Nicola Olivetti, and Dov Gabbay. Proof Theory for Fuzzy Logics. Springer Netherlands, 2009. URL: https://doi.org/10.1007/978-1-4020-9409-5.
  25. George Metcalfe, Francesco Paoli, and Constantine Tsinakis. Residuated structures in algebra and logic, volume 277 of Mathematical Surveys and Monographs. American Mathematical Society, Providence, RI, 2023. Google Scholar
  26. G. E. Minc. Some calculi of modal logic. Trudy Mat. Inst. Steklov, 98:88-111, 1968. Google Scholar
  27. Francesco Paoli. Substructural logics: a primer, volume 13 of Trends in Logic - Studia Logica Library. Kluwer Academic Publishers, Dordrecht, 2002. URL: https://doi.org/10.1007/978-94-017-3179-9.
  28. G. Pottinger. Uniform, cut-free formulations of T, S4 and S5 (abstract). J. of Symbolic Logic, 48(3):900, 1983. Google Scholar
  29. Revantha Ramanayake. Extended Kripke lemma and decidability for hypersequent substructural logics. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 795-806. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394802.
  30. Greg Restall. An Introduction to Substructural Logics. Routledge, 2000. Google Scholar
  31. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Trans. Comput. Theory, 8(1), February 2016. URL: https://doi.org/10.1145/2858784.
  32. Alasdair Urquhart. The complexity of decision procedures in relevance logic II. The Journal of Symbolic Logic, 64(4):1774-1802, 1999. URL: https://doi.org/10.2307/2586811.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact