The logic of bunched implications is undecidable

Nick Galatos, Peter Jipsen, Søren Brinck Knudstorp, Revantha Ramanayake

arXivarxiv/2603.01595Mar 2, 2026math.LOscore 0

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 {and, or, not, --*}-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and…

SourceJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2603.01595
curl -X POST /api/v1/records/arxiv/2603.01595/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2603.01595/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'