{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:27:34Z","timestamp":1759638454506},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027154"},{"type":"electronic","value":"9783642027161"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02716-1_22","type":"book-chapter","created":{"date-parts":[[2009,6,30]],"date-time":"2009-06-30T04:22:21Z","timestamp":1246335741000},"page":"295-309","source":"Crossref","is-referenced-by-count":21,"title":["Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Pinto","sequence":"first","affiliation":[]},{"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-540-73099-6_9","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"L. Buisman (Postniece)","year":"2007","unstructured":"Buisman (Postniece), L., Gor\u00e9, R.: A cut-free sequent calculus for bi-intuitionistic logic. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS, vol.\u00a04548, pp. 90\u2013106. Springer, Heidelberg (2007)"},{"issue":"1\u20132","key":"22_CR2","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0304-3975(99)00124-3","volume":"254","author":"T. Crolard","year":"2001","unstructured":"Crolard, T.: Subtractive logic. Theor. Comput. Sci.\u00a0254(1\u20132), 151\u2013185 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/351240.351262","volume-title":"Proc. of 5th Int. Conf. on Functional Programming, ICFP 2000","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, U.: The duality of computation. In: Proc. of 5th Int. Conf. on Functional Programming, ICFP 2000, Montreal, September 2000, pp. 233\u2013243. ACM Press, New York (2000)"},{"issue":"3","key":"22_CR4","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. of Symb. Logic\u00a057(3), 795\u2013807 (1992)","journal-title":"J. of Symb. Logic"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/BFb0018355","volume-title":"Category Theory and Computer Science","author":"A. Filinski","year":"1989","unstructured":"Filinski, A.: Declarative continuations: An investigation of duality in programming language semantics. In: Dybjer, P., Pitts, A.M., Pitt, D.H., Poign\u00e9, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol.\u00a0389, pp. 224\u2013249. Springer, Heidelberg (1989)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/10722086_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Gor\u00e9","year":"2000","unstructured":"Gor\u00e9, R.: Dual intuitionistic logic revisited. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol.\u00a01847, pp. 252\u2013267. Springer, Heidelberg (2000)"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R., Postniece, L.: Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic. J. of Logic and Comput. (to appear)","DOI":"10.1093\/logcom\/exn067"},{"key":"22_CR8","first-page":"43","volume-title":"Advances in Modal Logic 7","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: Areces, C., Goldblatt, R. (eds.) Advances in Modal Logic 7, pp. 43\u201366. College Publications, London (2008)"},{"key":"22_CR9","first-page":"80","volume":"25","author":"P. \u0141ukowski","year":"1996","unstructured":"\u0141ukowski, P.: Modal interpretation of Heyting-Brouwer logic. Bull. of Sect. of Logic\u00a025, 80\u201383 (1996)","journal-title":"Bull. of Sect. of Logic"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/3-540-52335-9_55","volume-title":"COLOG-88","author":"G. Mints","year":"1990","unstructured":"Mints, G.: Gentzen-type systems and resolution rules, part 1: Propositional logic. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 198\u2013231. Springer, Heidelberg (1990)"},{"key":"22_CR11","unstructured":"Monteiro, C.: Caracteriza\u00e7\u00f5es sem\u00e2nticas e dedutivas da l\u00f3gica bi-intuitionista. Master\u2019s thesis. Universidade de Tr\u00e1s-os-Montes e Alto-Douro (2006)"},{"issue":"5\u20136","key":"22_CR12","doi-asserted-by":"publisher","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. of Philos. Logic\u00a034(5\u20136), 507\u2013544 (2005)","journal-title":"J. of Philos. Logic"},{"key":"22_CR13","first-page":"225","volume-title":"Proc. of 2nd Gauss Symp.","author":"L. Pinto","year":"1995","unstructured":"Pinto, L., Dyckhoff, R.: Loop-free construction of counter-models for intuitionistic propositional logic. In: Behara, M., Fritsch, R., Lintz, R.G. (eds.) Proc. of 2nd Gauss Symp., Munich, August 1993, pp. 225\u2013232. Conf.\u00a0A. Walter de Gruyter, Berlin (1995)"},{"key":"22_CR14","doi-asserted-by":"crossref","first-page":"219","DOI":"10.4064\/fm-83-3-219-249","volume":"83","author":"C. Rauszer","year":"1974","unstructured":"Rauszer, C.: Semi-boolean algebras and their applications to intuitionistic logic with dual operators. Fund. Math.\u00a083, 219\u2013249 (1974)","journal-title":"Fund. Math."},{"issue":"1","key":"22_CR15","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF02120864","volume":"33","author":"C. Rauszer","year":"1974","unstructured":"Rauszer, C.: A formalization of the propositional calculus of H-B logic. Studia Logica\u00a033(1), 23\u201334 (1974)","journal-title":"Studia Logica"},{"issue":"1\u20132","key":"22_CR16","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BF02121115","volume":"36","author":"C. Rauszer","year":"1977","unstructured":"Rauszer, C.: Applications of Kripke models to Heyting-Brouwer logic. Studia Logica\u00a036(1\u20132), 61\u201371 (1977)","journal-title":"Studia Logica"},{"key":"22_CR17","unstructured":"Restall, G.: Extending intuitionistic logic with subtraction (unpublished note, 1997), \n                  \n                    http:\/\/consequently.org\/writing\/extendingj\/"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02716-1_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T10:55:54Z","timestamp":1619780154000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02716-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027154","9783642027161"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02716-1_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}