{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:28:48Z","timestamp":1725488928876},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_8","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"111-128","source":"Crossref","is-referenced-by-count":7,"title":["Connection-Based Proof Search in Propositional BI Logic"],"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"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/3-540-45744-5_21","volume-title":"First International Joint Conference on Automated Reasoning, IJCAR 2001","author":"P.A. Armelin","year":"2001","unstructured":"P.A. Armelin and D. Pym. Bunched logic programming (extended abstract). In First International Joint Conference on Automated Reasoning, IJCAR 2001, LNCS 2083, pages 289\u2013304, Siena, Italy, 2001."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"V. Balat and D. Galmiche. Labelled Deduction, volume 17 of Applied Logic Series, chapter Labelled Proof Systems for Intuitionistic Provability. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-94-011-4040-9_1"},{"issue":"4","key":"8_CR3","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"W. Bibel. On matrices with connections. Journal of ACM, 28(4):633\u2013645, 1981.","journal-title":"Journal of ACM"},{"issue":"3","key":"8_CR4","first-page":"486","volume":"4","author":"K. Broda","year":"1996","unstructured":"K. Broda, M. Finger, and A. Russo. LDS-natural deduction for substructural logics (extended abstract). Logic Journal of the IGPL, 4(3):486\u2013489, 1996.","journal-title":"Logic Journal of the IGPL"},{"issue":"1\u20132","key":"8_CR5","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/S0304-3975(99)00176-0","volume":"232","author":"D. Galmiche","year":"2000","unstructured":"D. Galmiche. Connection Methods in Linear Logic and Proof nets Construction. Theoretical Computer Science, 232(1\u20132):231\u2013272, 2000.","journal-title":"Theoretical Computer Science"},{"key":"8_CR6","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. Symp. 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. Symp. on Theoretical Aspects of Computer Software, TACS 2001, LNCS 2215, pages 263\u2013282, Sendai, Japan, 2001."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"S. Ishtiaq and P. O\u2019Hearn. BI as an assertion language for mutable data structures. In 28th ACM Symposium on Principles of Programming Languages, POPL 2001, pages 14\u201326, London, UK, 2001.","DOI":"10.1145\/373243.375719"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"C. Kreitz, H. Mantel, J. Otten, and S. Schmitt. Connection-based proof construction in linear logic. In 14th Int. Conference on Automated Deduction, pages 207\u2013221, Townsville, North Queensland, Australia, 1997.","DOI":"10.1007\/3-540-63104-6_20"},{"issue":"3","key":"8_CR9","first-page":"88","volume":"5","author":"C. Kreitz","year":"1999","unstructured":"C. Kreitz and J. Otten. Connection-based theorem proving in classical and non-classical logics. Journal of Universal Computer Science, 5(3):88\u2013112, 1999.","journal-title":"Journal of Universal Computer Science"},{"key":"8_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/3-540-48959-2_19","volume-title":"Typed Lambda Calculi and Applications, TLCA\u201999","author":"P. OHearn","year":"1999","unstructured":"P. O\u2019Hearn. Resource interpretations, bunched implications and the \u03b1\u03bb-calculus. In Typed Lambda Calculi and Applications, TLCA\u201999, LNCS 581, pages 258\u2013279, L\u2019Aquila, Italy, 1999."},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P.W. OHearn","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":"8_CR12","doi-asserted-by":"crossref","unstructured":"D. Pym. On bunched predicate logic. In 14h Symposium on Logic in Computer Science, pages 183\u2013192, Trento, Italy, July 1999. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1999.782614"},{"issue":"3","key":"8_CR13","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M. E. Stickel","year":"1981","unstructured":"M. E. Stickel. A unification algorithm for associative-commutative functions. Journal of ACM, 28(3):423\u2013434, 1981.","journal-title":"Journal of ACM"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"159","DOI":"10.2307\/2272559","volume":"37","author":"A. Urquhart","year":"1972","unstructured":"A. Urquhart. Semantics for relevant logic. Journal of Symbolic Logic, 37:159\u2013169, 1972.","journal-title":"Journal of Symbolic Logic"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"A. Voronkov. Proof-search in intuitionistic logic based on constraint satisfaction. In Int. Workshop Tableaux\u201996, LNAI 1071, pages 312\u2013327, Terrasini, Italy, 1996.","DOI":"10.1007\/3-540-61208-4_20"},{"key":"8_CR16","unstructured":"L.A. Wallen. Automated Proof search in Non-Classical Logics. MIT Press, 1990."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:55:45Z","timestamp":1556754945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}