Document Open Access Logo

The Logic of Bunched Implications Is Undecidable

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.46.pdf
  • Filesize: 1.05 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
  • Theory of computation → Linear logic
  • Theory of computation → Proof theory
  • Theory of computation → Logic and verification
  • Theory of computation → Algebraic semantics
  • Theory of computation → Turing machines
Keywords
  • Bunched implication logic
  • Intuitionistic logic with operators
  • Residuated lattices
  • Substructural logics
  • Undecidable logics
  • Tiling problem

Metrics

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

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

Author Details

Nikolaos Galatos
  • University of Denver, CO, USA
Peter Jipsen
  • Chapman University, Orange, CA, USA
Søren Brinck Knudstorp
  • ILLC and Philosophy, University of Amsterdam, The Netherlands
Revantha Ramanayake
  • University of Groningen, The Netherlands

Funding

  • Knudstorp, Søren Brinck: Supported in part by the MOSAIC project (H2020-MSCA-RISE-2020, 101007627), and in part by the Nothing is Logical (NihiL) project (NWO OC 406.21.CTW.023).
  • Ramanayake, Revantha: Supported in part by the Dutch Research Council (NWO) project OCENW.M.22.258.

Acknowledgements

We thank the anonymous referees for their close reading and helpful comments.

References

  1. Robert Berger. The Undecidability of the Domino Problem, volume 66 of Memoirs of the American Mathematical Society. American Mathematical Society, Providence, RI, 1966. URL: https://doi.org/10.1090/memo/0066.
  2. Stephen Brookes. A semantics for concurrent separation logic. Theoretical Computer Science, 375(1-3):227-270, April 2007. URL: https://doi.org/10.1016/j.tcs.2006.12.034.
  3. Stephen Brookes and Peter W. O'Hearn. Concurrent separation logic. ACM SIGLOG News, 3(3):47-65, August 2016. URL: https://doi.org/10.1145/2984450.2984457.
  4. James Brotherston and Max Kanovich. Undecidability of propositional separation logic and its neighbours. J. ACM, 61(2):14:1-14:43, April 2014. URL: https://doi.org/10.1145/2542667.
  5. James Brotherston and Max I. Kanovich. Undecidability of propositional separation logic and its neighbours. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 130-139, 2010. URL: https://doi.org/10.1109/LICS.2010.24.
  6. Cristiano Calcagno and Dino Distefano. Infer: An automatic program verifier for memory safety of C programs. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, Proceedings of Third International Symposium on NASA Formal Methods (NFM), pages 459-465. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-20398-5_33.
  7. Simon Docherty and David Pym. Stone-type dualities for separation logics. Logical Methods in Computer Science, Volume 15, Issue 1, March 2019. URL: https://doi.org/10.23638/LMCS-15(1:27)2019.
  8. Nick Galatos, Peter Jipsen, Søren Brinck Knudstorp, and Revantha Ramanayake. The logic of bunched implications is undecidable, 2026. URL: https://arxiv.org/abs/2603.01595.
  9. Nikolaos Galatos and Peter Jipsen. Distributive residuated frames and generalized bunched implication algebras. Algebra Universalis, 78:303-336, 2017. Google Scholar
  10. Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Number 151 in Studies in Logic and the Foundations of Mathematics. Elsevier, 2007. Google Scholar
  11. Didier Galmiche, Daniel Méry, and David J. Pym. The semantics of BI and resource tableaux. Mathematical Structures in Computer Science, 15(6):1033-1088, 2005. URL: https://doi.org/10.1017/S0960129505004858.
  12. Infer. A tool to detect bugs in Java and C/C++/Objective-C code before it ships. URL: https://fbinfer.com/.
  13. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Chris Hankin and Dave Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, pages 14-26. ACM, 2001. URL: https://doi.org/10.1145/360204.375719.
  14. Peter Jipsen and Tadeusz Litak. An Algebraic Glimpse at Bunched Implications and Separation Logic, pages 185-242. Springer International Publishing, Cham, 2022. URL: https://doi.org/10.1007/978-3-030-76920-8_5.
  15. Bjarni Jónsson and Constantine Tsinakis. Relation algebras as residuated boolean algebras. Algebra Univeralis, 30(4):469-478, 1993. Google Scholar
  16. Bjarni Jónsson and Alfred Tarski. Boolean algebras with operators. Part I. American Journal of Mathematics, 73(4):891-939, 1951. URL: http://www.jstor.org/stable/2372123.
  17. M. Kaminski and N. Francez. The lambek calculus extended with intuitionistic propositional logic. Stud Logica, 104:1051-1082, 2016. URL: https://doi.org/10.1007/s11225-016-9665-0.
  18. Søren Brinck Knudstorp. Relevant 𝐒 is undecidable. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '24), pages 1-8, Tallinn, Estonia, 2024. ACM. URL: https://doi.org/10.1145/3661814.3662128.
  19. Søren Brinck Knudstorp. Diamonds and dominoes: Impossibility results for associative modal logics, 2025. Under review. URL: https://arxiv.org/abs/2506.16366.
  20. Søren Brinck Knudstorp. Undecidability in relevant logic, 2025. Manuscript. Google Scholar
  21. MichałKozak. Distributive full Lambek calculus has the finite model property. Studia Logica, 91(2):201-216, 2009. URL: https://doi.org/10.1007/s11225-009-9172-7.
  22. Á. Kurucz, I. Németi, I. Sain, and A. Simon. Decidable and undecidable logics with a binary modality. Journal of Logic, Language, and Information, 4(3):191-206, 1995. URL: https://doi.org/10.1007/BF01049412.
  23. Dominique Larchey-Wendling and Didier Galmiche. The undecidability of boolean BI through phase semantics. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 140-149, 2010. URL: https://doi.org/10.1109/LICS.2010.18.
  24. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. The Bulletin of Symbolic Logic, 5(2):215-244, 1999. URL: https://doi.org/10.2307/421090.
  25. David Pym. A summary of the more recent papers on the completeness of the logic of bunched implications. https://www.cantab.net/users/david.pym/BI-completeness-papers.pdf, 2025. Accessed: 2026-01-03.
  26. David J. Pym, Peter W. O'Hearn, and Hongseok Yang. Possible worlds and resources: the semantics of BI. Theoretical Computer Science, 315(1):257-305, 2004. URL: https://doi.org/10.1016/j.tcs.2003.11.020.
  27. John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, pages 303-321. Palgrave, 2000. Google Scholar
  28. John C. Reynolds. Separation Logic: A logic for shared mutable data structures. In Proceedings of 17th IEEE Symposium on Logic in Computer Science (LICS), pages 55-74, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  29. Alasdair Urquhart. Duality for algebras of relevant logics. Studia Logica, 56(1-2):263-276, 1996. Special issue on Priestley duality. URL: https://doi.org/10.1007/BF00370149.
  30. Hao Wang. Dominoes and the ∀∃∀ case of the decision problem. In Mathematical Theory of Automata, pages 23-55. Polytechnic Press, 1963. Google Scholar
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