{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:22Z","timestamp":1725573082047},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540252368"},{"type":"electronic","value":"9783540322757"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_31","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:14:41Z","timestamp":1292879681000},"page":"466-480","source":"Crossref","is-referenced-by-count":4,"title":["The Inverse Method for the Logic of Bunched Implications"],"prefix":"10.1007","author":[{"given":"Kevin","family":"Donnelly","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tyler","family":"Gibson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neel","family":"Krishnaswami","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Magill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sungwoo","family":"Park","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"31_CR1","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation\u00a02(3), 197\u2013347 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Armel\u00edn, P.: Logic programming with bunched logic. PhD thesis, University of London (2002)","DOI":"10.1007\/3-540-45744-5_21"},{"key":"31_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/3-540-45744-5_21","volume-title":"Automated Reasoning","author":"P.A. Armel\u00edn","year":"2001","unstructured":"Armel\u00edn, P.A., Pym, D.J.: Bunched logic programming. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 289\u2013304. Springer, Heidelberg (2001)"},{"key":"31_CR4","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, ch. 2, pp. 19\u2013100. North Holland, Amsterdam (2001)"},{"key":"31_CR5","unstructured":"Beal, F., M\u00e9ry, D., Galmiche, D.: Bill: A theorem prover for propositional bi logic"},{"key":"31_CR6","unstructured":"Chaudhuri, K., Pfenning, F.: Resource management for the inverse method in linear logic. Carnegie Mellon University, Unpublished Maniscript (January 2003)"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, pp. 179\u2013272. Elsevier Science and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50006-0"},{"key":"31_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/3-540-45793-3_13","volume-title":"Computer Science Logic","author":"D. Galmiche","year":"2002","unstructured":"Galmiche, D., M\u00e9ry, D., Pym, D.J.: Resource tableaux. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 183\u2013199. Springer, Heidelberg (2002)"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Galmiche, D., M\u00e9ry, D.: Semantic labelled tableaux for propositional bi (without bottom). Journal of Logic and Computation\u00a013(5) (October 2003)","DOI":"10.1093\/logcom\/13.5.707"},{"key":"31_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"31_CR11","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/601775.601778","volume":"4","author":"J. Harland","year":"2003","unstructured":"Harland, J., Pym, D.: Resource-distribution via boolean constraints. ACM Trans. Comput. Logic\u00a04(1), 56\u201390 (2003)","journal-title":"ACM Trans. Comput. Logic"},{"key":"31_CR12","first-page":"1420","volume":"5","author":"S. Maslov","year":"1964","unstructured":"Maslov, S.: The inverse method of establishing deducibility in classical predicate calculus. Soviet Mathematical Doklady\u00a05, 1420\u20131424 (1964)","journal-title":"Soviet Mathematical Doklady"},{"issue":"2","key":"31_CR13","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P.W. O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic\u00a05(2), 215\u2013244 (1999)","journal-title":"Bulletin of Symbolic Logic"},{"key":"31_CR14","unstructured":"Pfenning, F.: The inverse method. Carnegie Mellon University, Lecture Notes, Ch. 5 (February 2004)"},{"key":"31_CR15","series-title":"Applied Logic Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0091-7","volume-title":"The Semantics and Proof Theory of the Logic of the Logic of Bunched Implications","author":"D.J. Pym","year":"2002","unstructured":"Pym, D.J.: The Semantics and Proof Theory of the Logic of the Logic of Bunched Implications. Applied Logic Series, vol.\u00a026. Kluwer Academic Publishers, Dordrecht (2002), Errata and Remarks maintained at: http:\/\/www.cs.bath.ac.uk\/pym\/BI-monograph-errata.pdf"},{"key":"31_CR16","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"issue":"3","key":"31_CR17","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/BF00885763","volume":"12","author":"T. Tammet","year":"1994","unstructured":"Tammet, T.: Proof strategies in linear logic. Journal of Automated Reasoning\u00a012(3), 273\u2013304 (1994)","journal-title":"Journal of Automated Reasoning"},{"key":"31_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-61511-3_65","volume-title":"Automated Deduction - Cade-13","author":"T. Tammet","year":"1996","unstructured":"Tammet, T.: A resolution theorem prover for intuitionistic logic. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 2\u201316. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32275-7_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:35:13Z","timestamp":1605760513000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}