{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:13:59Z","timestamp":1760044439805},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442400"},{"type":"electronic","value":"9783540457930"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45793-3_13","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T12:03:26Z","timestamp":1187265806000},"page":"183-199","source":"Crossref","is-referenced-by-count":8,"title":["Resource Tableaux"],"prefix":"10.1007","author":[{"given":"Didier","family":"Galmiche","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"M\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pym","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"V. Balat and D. Galmiche. Labelled Deduction, in Volume 17 of Applied Logic Series, Labelled Proof Systems for Intuitionistic Provability. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-94-011-4040-9_1"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"D. M. Gabbay. Labelled Deductive Systems. OUP, 1996.","DOI":"10.1093\/oso\/9780198538332.001.0001"},{"key":"13_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/3-540-45500-0_13","volume-title":"4th Int. Symposium on Theoretical Aspects of Computer Software, TACS 2001","author":"D. Galmiche","year":"2001","unstructured":"D. Galmiche and D. M\u00e9ry. Proof-search and countermodel generation in propositional BI logic-extended abstract-. In 4th Int. Symposium on Theoretical Aspects of Computer Software, TACS 2001, LNCS 2215, 263\u2013282, Sendai, Japan, 2001. Full version submitted."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"J. Harland and D. Pym. Resource-distribution via Boolean Constraints (Extended Abstract). In 14th Int. Conference on Automated Deduction, CADE-12, LNAI 814, 222\u2013236, Townsville, Queensland, Australia, July 1997. Full version to appear in ACM ToCL, 2003.","DOI":"10.1007\/3-540-63104-6_21"},{"issue":"4","key":"13_CR6","doi-asserted-by":"publisher","first-page":"1202","DOI":"10.2307\/2275637","volume":"62","author":"Y. Lafont","year":"1997","unstructured":"Y. Lafont. The finite model property for various fragments of linear logic. J. Symb. Logic 62(4):1202\u20131208, 1997.","journal-title":"J. Symb. Logic"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"P. Lincoln. Deciding provability of linear logic formulas. In Advances in Linear Logic, J.-Y. Girard, Y. Lafont and L. Regnier (editors), Cambridge Univ. Press, 1995, 109\u2013122.","DOI":"10.1017\/CBO9780511629150.006"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"S. Ishtiaq and P. O\u2019Hearn. BI as an assertion language for mutable data structures. In Proc. 28th ACM Symp. on Principles of Prog. Langs., POPL 2001, 14\u201326, London, UK, 2001.","DOI":"10.1145\/373243.375719"},{"key":"13_CR9","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proc. 15th Int. Workshop on Computer Science Logic, CSL\u201901","author":"P. O\u2019Hearn","year":"2001","unstructured":"P. O\u2019Hearn and J. Reynolds and H. Yang. Local Reasoning about Programs that Alter Data Structures. In Proc. 15th Int. Workshop on Computer Science Logic, CSL\u201901, LNCS 2142, 1\u201319, Paris, 2001."},{"issue":"2","key":"13_CR10","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P. W. O\u2019Hearn","year":"1999","unstructured":"P. W. O\u2019Hearn and D. Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2):215\u2013244, 1999.","journal-title":"Bulletin of Symbolic Logic"},{"key":"13_CR11","unstructured":"M. Okada and K. Terui. Completeness proofs for linear logic based on proof search method (preliminary report). In Type theory and its applications to computer systems, 57\u201375, RIMS, Kyoto University, 1998."},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"D. Pym. On bunched predicate logic. In Proc. 14th Symposium on Logic in Computer Science, 183\u2013192, Trento, Italy, July 1999. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1999.782614"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"D. J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer Academic Publishers, 2002. To appear; preprint available at http:\/\/www.cs.bath.ac.uk\/~pyni\/recent.html .","DOI":"10.1007\/978-94-017-0091-7"},{"key":"13_CR14","unstructured":"D. J. Pym, P. W. O\u2019Hearn and H. Yang. Possible Worlds and Resources: The Semantics of BI. Manuscript, http:\/\/www.cs.bath.ac.uk\/~pym\/recent.html ."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45793-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T12:17:23Z","timestamp":1708172243000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45793-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442400","9783540457930"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45793-3_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}