The logic of bunched implications (BI), introduced by O'Hearn and Pym, is a substructural logic which freely combines additive and multiplicative implications. Boolean BI (BBI) denotes BI with classical interpretation of additives and its model is the commutative monoid. We show that when the monoid is finitely generated and propositions are recursively defined, or the monoid is infinitely generated and propositions are restricted to generator propositions, the model checking problem is undecidable. In the case of finitely related monoid and generator propositions, the model checking problem is EXPSPACE-complete. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Guo, H., Wang, H., Xu, Z., & Cao, Y. (2009). On model checking boolean BI. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5771 LNCS, pp. 302–316). https://doi.org/10.1007/978-3-642-04027-6_23
Mendeley helps you to discover research relevant for your work.