{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:20:10Z","timestamp":1781652010079,"version":"3.54.5"},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,3,8]],"date-time":"2013-03-08T00:00:00Z","timestamp":1362700800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1007\/s10817-013-9279-4","type":"journal-article","created":{"date-parts":[[2013,3,7]],"date-time":"2013-03-07T02:32:56Z","timestamp":1362623576000},"page":"3-26","source":"Crossref","is-referenced-by-count":2,"title":["A Connection-based Characterization of Bi-intuitionistic Validity"],"prefix":"10.1007","volume":"51","author":[{"given":"Didier","family":"Galmiche","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"M\u00e9ry","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2013,3,8]]},"reference":[{"key":"9279_CR1","doi-asserted-by":"crossref","unstructured":"Antonsen, R., Waaler, A.: A labelled system for IPL with variable splitting. In: 21st Int. Conference on Automated Deduction, CADE-21. LNAI, vol.\u00a04603, Bremen, Germany, pp.\u00a0132\u2013146. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_10"},{"key":"9279_CR2","doi-asserted-by":"crossref","unstructured":"Avron, A., Lahav, O.: Kripke semantics for basic sequent systems. In: Int. Conference on Analytic Tableaux and Related Methods, TABLEAUX 2011. LNAI, vol.\u00a06793, Bern, Switzerland, pp.\u00a043\u201357. Springer (2011)","DOI":"10.1007\/978-3-642-22119-4_6"},{"issue":"1\u20132","key":"9279_CR3","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/S0304-3975(99)00124-3","volume":"254","author":"T Crolard","year":"2001","unstructured":"Crolard, T.: Substractive logic. Theor. Comp. Sci. 254(1\u20132), 151\u2013185 (2001)","journal-title":"Theor. Comp. Sci."},{"issue":"4","key":"9279_CR4","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1093\/logcom\/14.4.529","volume":"14","author":"T Crolard","year":"2004","unstructured":"Crolard, T.: A formulae-as-types interpretation of substractive logic. J. Log. Comput. 14(4), 529\u2013570 (2004)","journal-title":"J. Log. Comput."},{"key":"9279_CR5","doi-asserted-by":"crossref","unstructured":"Galmiche, D., M\u00e9ry, D.: Characterizing provability in BI\u2019s pointer logic through resource graphs. In: Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005. LNAI, vol.\u00a03835, Montego Bay, Jamaica, pp.\u00a0459\u2013473. Springer (2005)","DOI":"10.1007\/11591191_32"},{"issue":"3","key":"9279_CR6","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/j.entcs.2004.06.069","volume":"125","author":"D Galmiche","year":"2005","unstructured":"Galmiche, D., M\u00e9ry, D.: Resource graphs and countermodels in resource logics. Electron. Notes Theor. Comp. Sci. 125(3), 117\u2013135 (2005)","journal-title":"Electron. Notes Theor. Comp. Sci."},{"key":"9279_CR7","doi-asserted-by":"crossref","unstructured":"Galmiche, D., M\u00e9ry, D.: A connection-based characterization of bi-intuitionistic validity. In: 23rd Int. Conference on Automated Deduction, CADE-23. LNAI, vol.\u00a06803, Wroclaw, Poland, pp.\u00a0268\u2013282. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_21"},{"issue":"1","key":"9279_CR8","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1093\/logcom\/exn067","volume":"20","author":"R Gor\u00e9","year":"2010","unstructured":"Gor\u00e9, R., Postniece, L.: Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic. J. Log. Comput. 20(1), 233\u2013260 (2010)","journal-title":"J. Log. Comput."},{"key":"9279_CR9","first-page":"43","volume-title":"Advances in Modal Logic","author":"R Gor\u00e9","year":"2008","unstructured":"Gor\u00e9, R., Postniece, L., Tiu, A.: Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In: Advances in Modal Logic, vol.\u00a07, pp.\u00a043\u201366. College Publications, London (2008)"},{"issue":"5\u20136","key":"9279_CR10","doi-asserted-by":"crossref","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. J. Philos. Logic 34(5\u20136), 507\u2013554 (2005)","journal-title":"J. Philos. Logic"},{"key":"9279_CR11","doi-asserted-by":"crossref","unstructured":"Otten, J., Kreitz, C.: T-string-unification: unifying prefixes in non classical proof methods. In: 5th Int. Workshop on Analytic Tableaux and Related Methods, TABLEAUX\u201996. LNAI, vol.\u00a01071, Terrasini, Palermo, Italy, pp.\u00a0244\u2013260. Springer (1996)","DOI":"10.1007\/3-540-61208-4_16"},{"key":"9279_CR12","doi-asserted-by":"crossref","unstructured":"Pinto, L., Uustalu, T.: Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents. In: Int. Conference on Analytic Tableaux and Related Methods, TABLEAUX 2009. LNAI, vol.\u00a05607, Oslo, Norway, pp.\u00a0295\u2013309. Springer (2009)","DOI":"10.1007\/978-3-642-02716-1_22"},{"key":"9279_CR13","doi-asserted-by":"crossref","unstructured":"Postniece, L.: Deep inference in bi-intuitionistic logic. In: Int Workshop on Logic, Language, Information and Computation, WoLLIC 2009. LNAI, vol.\u00a05514, Tokyo, Japan, pp.\u00a0320\u2013334. Springer (2009)","DOI":"10.1007\/978-3-642-02261-6_26"},{"key":"9279_CR14","first-page":"1","volume":"167","author":"C Rauszer","year":"1980","unstructured":"Rauszer, C.: An algebraic and Kripke-style approach to a certain extension of intuitionistic logic. Diss. Math. 167, 1\u201362 (1980)","journal-title":"Diss. Math."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9279-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9279-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9279-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,10]],"date-time":"2019-07-10T11:47:41Z","timestamp":1562759261000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9279-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,8]]},"references-count":14,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["9279"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9279-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,8]]}}}