{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T05:36:37Z","timestamp":1757309797433},"reference-count":24,"publisher":"Oxford University Press (OUP)","issue":"4","license":[{"start":{"date-parts":[[2017,1,17]],"date-time":"2017-01-17T00:00:00Z","timestamp":1484611200000},"content-version":"vor","delay-in-days":588,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,6,7]]},"DOI":"10.1093\/logcom\/exv033","type":"journal-article","created":{"date-parts":[[2015,6,10]],"date-time":"2015-06-10T23:02:33Z","timestamp":1433977353000},"page":"809-872","source":"Crossref","is-referenced-by-count":1,"title":["A labelled sequent calculus for BBI: proof theory and proof search"],"prefix":"10.1093","volume":"28","author":[{"given":"Zh\u00e9","family":"H\u00f3u","sequence":"first","affiliation":[{"name":"Research School of Computer Science, The Australian National University, Canberra, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[{"name":"Research School of Computer Science, The Australian National University, Canberra, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[{"name":"School of Computer Engineering, Nanyang Technological University, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2015,6,9]]},"reference":[{"key":"key\n\t\t\t\t20180607120739_B1","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1023\/A:1013886427723","article-title":"Free-variable tableaux for propositional modal logics","volume":"69","author":"Beckert","year":"2001","journal-title":"Studia Logica"},{"key":"key\n\t\t\t\t20180607120739_B2","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/j.entcs.2010.08.012","article-title":"A unified display proof theory for bunched logic","volume":"265","author":"Brotherston","year":"2010","journal-title":"Electronic Notes in Theoretical Computer Science (ENTCS)"},{"key":"key\n\t\t\t\t20180607120739_B3","article-title":"Classical BI: its semantics and proof theory","volume":"6","author":"Brotherston","year":"2010","journal-title":"Logical Methods in Computer Science (LMCS)"},{"key":"key\n\t\t\t\t20180607120739_B4","first-page":"130","article-title":"Undecidability of propositional separation logic and its neighbours","volume-title":"LICS","author":"Brotherston","year":"2010"},{"issue":"14","key":"key\n\t\t\t\t20180607120739_B5","article-title":"Undecidability of propositional separation logic and its neighbours","volume":"61","author":"Brotherston","year":"2014","journal-title":"Journal of the Association for Computing Machinery (ACM)"},{"key":"key\n\t\t\t\t20180607120739_B6","first-page":"453","article-title":"Parametric completeness for separation theories","volume-title":"POPL","author":"Brotherston","year":"2014"},{"key":"key\n\t\t\t\t20180607120739_B7","first-page":"366","article-title":"Local action and abstract separation logic","volume-title":"LICS","author":"Calcagno","year":"2007"},{"key":"key\n\t\t\t\t20180607120739_B8","doi-asserted-by":"crossref","DOI":"10.1145\/1656242.1656244","article-title":"Deciding security properties for cryptographic protocols: application to key cycles","volume":"11","author":"Comon-Lundh","year":"2010","journal-title":"ACM Transactions on Computational Logic"},{"key":"key\n\t\t\t\t20180607120739_B9","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-642-10672-9_13","article-title":"A fresh look at separation algebras and share accounting","volume-title":"Asian Symposium on Programming Languages and Systems (APLAS)","author":"Dockins","year":"2009"},{"key":"key\n\t\t\t\t20180607120739_B10","first-page":"358","article-title":"Expressivity properties of Boolean {BI} through relational models","volume-title":"Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"Galmiche","year":"2006"},{"key":"key\n\t\t\t\t20180607120739_B11","first-page":"435","article-title":"Comparing unification algorithms in first-order theorem proving","volume-title":"KI: Annual Conference on Artificial Intelligence","author":"Hoder","year":"2009"},{"key":"key\n\t\t\t\t20180607120739_B12","first-page":"465","article-title":"Proof search for propositional abstract separation logics via labelled sequents","volume-title":"POPL","author":"Hou","year":"2014"},{"key":"key\n\t\t\t\t20180607120739_B13","article-title":"The formal strong completeness of partial monoidal Boolean BI","author":"Larchey-Wendling","year":"2014","journal-title":"Journal of Logic and Computation"},{"key":"key\n\t\t\t\t20180607120739_B14","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1017\/S0960129509007567","article-title":"Exploring the relation between intuitionistic BI and Boolean BI: an unexpected embedding","volume":"19","author":"Larchey-Wendling","year":"2009","journal-title":"Mathematical Structures in Computer Science"},{"key":"key\n\t\t\t\t20180607120739_B15","first-page":"140","article-title":"The undecidability of Boolean BI through phase semantics","volume":"1","author":"Larchey-Wendling","year":"2010","journal-title":"Logic in Computer Science"},{"key":"key\n\t\t\t\t20180607120739_B16","doi-asserted-by":"crossref","DOI":"10.1145\/2422085.2422091","article-title":"Non-deterministic phase semantics and the undecidability of Boolean BI","volume":"14","author":"Larchey-Wendling","year":"2013","journal-title":"ACM Transactions on Computational Logic"},{"key":"key\n\t\t\t\t20180607120739_B17","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","article-title":"Proof analysis in modal logic","volume":"34","author":"Negri","year":"2005","journal-title":"Journal of Philosophical Logic"},{"key":"key\n\t\t\t\t20180607120739_B18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"Negri","year":"2001"},{"key":"key\n\t\t\t\t20180607120739_B19","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","article-title":"The logic of bunched implications","volume":"5","author":"O'Hearn","year":"1999","journal-title":"Bulletin of Symbolic Logic"},{"key":"key\n\t\t\t\t20180607120739_B20","first-page":"219","article-title":"A theorem prover for Boolean BI","author":"Park","year":"2013","journal-title":"POPL: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '13)"},{"key":"key\n\t\t\t\t20180607120739_B21","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0091-7","volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","author":"Pym","year":"2002"},{"key":"key\n\t\t\t\t20180607120739_B22","first-page":"55","volume-title":"Separation logic: a logic for shared mutable data structures","author":"Reynolds","year":"2002"},{"key":"key\n\t\t\t\t20180607120739_B23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-6(3:12)2010","article-title":"A proof theoretic analysis of intruder theories","volume":"6","author":"Tiu","year":"2010","journal-title":"Logical Methods in Computer Science"},{"key":"key\n\t\t\t\t20180607120739_B24","volume-title":"Basic Proof Theory","author":"Troelstra","year":"1996"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/28\/4\/809\/25020937\/exv033.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,26]],"date-time":"2019-08-26T11:26:51Z","timestamp":1566818811000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/28\/4\/809\/2917811"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,9]]},"references-count":24,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2015,6,9]]},"published-print":{"date-parts":[[2018,6,7]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exv033","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2018,6]]},"published":{"date-parts":[[2015,6,9]]}}}