2026-07-20T11:32:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26833 2026-07-09T11:31:09Z ddc:004 open_access

The Logic of Bunched Implications Is Undecidable Galatos, Nikolaos Jipsen, Peter Knudstorp, Søren Brinck Ramanayake, Revantha Bunched implication logic Intuitionistic logic with operators Residuated lattices Substructural logics Undecidable logics Tiling problem 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nikolaos Galatos and Peter Jipsen and Søren Brinck Knudstorp and Revantha Ramanayake 2026 Is Part Of LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.LICS.2026.46 urn:nbn:de:0030-drops-268334 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.46 eng https://creativecommons.org/licenses/by/4.0/legalcode