{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,25]],"date-time":"2025-05-25T10:02:18Z","timestamp":1748167338499},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642405365"},{"type":"electronic","value":"9783642405372"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40537-2_16","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T08:33:51Z","timestamp":1378888431000},"page":"172-187","source":"Crossref","is-referenced-by-count":8,"title":["A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search"],"prefix":"10.1007","author":[{"given":"Zh\u00e9","family":"H\u00f3u","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","first-page":"197","volume":"265","author":"J. Brotherston","year":"2010","unstructured":"Brotherston, J.: A unified display proof theory for bunched logic. ENTCS\u00a0265, 197\u2013211 (2010)","journal-title":"ENTCS"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Calcagno, C.: Classical BI: Its semantics and proof theory. LMCS\u00a06(3) (2010)","DOI":"10.2168\/LMCS-6(3:3)2010"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. In: LICS, pp. 130\u2013139 (2010)","DOI":"10.1109\/LICS.2010.24"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. Submitted to the Journal of ACM (2013)","DOI":"10.1145\/2542667"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11944836_33","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"D. Galmiche","year":"2006","unstructured":"Galmiche, D., Larchey-Wendling, D.: Expressivity properties of boolean BI through relational models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol.\u00a04337, pp. 357\u2013368. Springer, Heidelberg (2006)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-642-04617-9_55","volume-title":"KI 2009: Advances in Artificial Intelligence","author":"K. Hoder","year":"2009","unstructured":"Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS, vol.\u00a05803, pp. 435\u2013443. Springer, Heidelberg (2009)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"H\u00f3u, Z., Tiu, A., Gor\u00e9, R.: A labelled sequent calculus for BBI: Proof theory and proof search. arXiv:1302.4783 (2013)","DOI":"10.1007\/978-3-642-40537-2_16"},{"key":"16_CR8","unstructured":"Larchey-Wendling, D.: The formal strong completeness of partial monoidal boolean BI. Submitted to Journal of Logic and Computation (2012)"},{"issue":"3","key":"16_CR9","first-page":"435","volume":"19","author":"D. Larchey-Wendling","year":"2009","unstructured":"Larchey-Wendling, D., Galmiche, D.: Exploring the relation between intuitionistic BI and boolean BI: An unexpected embedding. MSCS\u00a019(3), 435\u2013500 (2009)","journal-title":"MSCS"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling, D., Galmiche, D.: The undecidability of boolean BI through phase semantics. In: LICS, pp. 140\u2013149 (2010)","DOI":"10.1109\/LICS.2010.18"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling, D., Galmiche, D.: Non-deterministic phase semantics and the undecidability of boolean BI. ACM TOCL\u00a014(1) (2013)","DOI":"10.1145\/2422085.2422091"},{"issue":"5-6","key":"16_CR12","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","volume":"34","author":"S. Negri","year":"2005","unstructured":"Negri, S.: Proof analysis in modal logic. JPL\u00a034(5-6), 507\u2013544 (2005)","journal-title":"JPL"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Negri, S., von Plato, J.: Structural Proof Theory. CUP (2001)","DOI":"10.1017\/CBO9780511527340"},{"issue":"2","key":"16_CR14","first-page":"215","volume":"5","author":"P.W. O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. BSL\u00a05(2), 215\u2013244 (1999)","journal-title":"BSL"},{"key":"16_CR15","first-page":"219","volume-title":"POPL 2013","author":"J. Park","year":"2013","unstructured":"Park, J., Seo, J., Park, S.: A theorem prover for boolean BI. In: POPL 2013, pp. 219\u2013232. ACM, New York (2013)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Pym, D.J.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer Academic Publishers (2002)","DOI":"10.1007\/978-94-017-0091-7"},{"key":"16_CR17","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE Computer Society (2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40537-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T01:48:28Z","timestamp":1558057708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40537-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405365","9783642405372"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40537-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}