{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:19:33Z","timestamp":1763641173213},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730989"},{"type":"electronic","value":"9783540730996"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73099-6_9","type":"book-chapter","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T03:04:02Z","timestamp":1189739042000},"page":"90-106","source":"Crossref","is-referenced-by-count":10,"title":["A Cut-Free Sequent Calculus for Bi-intuitionistic Logic"],"prefix":"10.1007","author":[{"given":"Linda","family":"Buisman","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Proc. Logic Colloquium, Keele, UK, 1993, pp. 1\u201332, OUP (1996)"},{"key":"9_CR2","unstructured":"Buisman, L., Gor\u00e9, R.: A cut-free sequent calculus for bi-intuitionistic logic: extended version (2007), http:\/\/arxiv.org\/abs\/0704.1707"},{"issue":"1\u20132","key":"9_CR3","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. Comp. Sci.\u00a0254(1\u20132), 151\u2013185 (2001)","journal-title":"Theor. Comp. Sci."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Czermak, J.: A remark on Gentzen\u2019s calculus of sequents. NDJFL 18(3) (1977)","DOI":"10.1305\/ndjfl\/1093888021"},{"key":"9_CR5","volume-title":"Translations of Mathematical Monographs","author":"A. Dragalin","year":"1988","unstructured":"Dragalin, A.: Mathematical Intuitionism: Introduction to Proof Theory. In: Translations of Mathematical Monographs, vol.\u00a068, Cambridge Univ. Press, Cambridge (1988)"},{"issue":"3","key":"9_CR6","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. The Journal of Symbolic Logic\u00a057(3), 795\u2013807 (1992)","journal-title":"The Journal of Symbolic Logic"},{"key":"9_CR7","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-94-017-1754-0_6","volume-title":"Handbook of Tableau Methods","author":"R. Gor\u00e9","year":"1999","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, et al. (eds.) Handbook of Tableau Methods, pp. 297\u2013396. Kluwer, Dordrecht (1999)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"A. Heuerding","year":"1996","unstructured":"Heuerding, A., Seyfried, M., Zimmermann, H.: Efficient loop-check for backward proof search in some non-classical propositional logics. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, Springer, Heidelberg (1996)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Horrocks, I., Sattler, U., Tobies, S.: A PSpace-algorithm for deciding ${ALCNI}_{R^+}$ -satisfiability. LTCS-98-08, LuFG Theor. Comp. Sci, RWTH Aachen (1998)","DOI":"10.25368\/2022.84"},{"key":"9_CR10","unstructured":"Howe, J.M.: Proof search issues in some non-classical logics. PhD thesis, University of St Andrews (1998)"},{"key":"9_CR11","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, 23\u201334 (1974)","journal-title":"Studia Logica"},{"key":"9_CR12","unstructured":"Rauszer, C.: An algebraic and Kripke-style approach to a certain extension of intuitionistic logic. Dissertationes Mathematicae, 168, Inst. of Math, Polish Academy of Sciences (1980)"},{"key":"9_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-69778-0_28","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Schwendimann","year":"1998","unstructured":"Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, Springer, Heidelberg (1998)"},{"issue":"1","key":"9_CR14","first-page":"159","volume":"47","author":"V. \u015avejdar","year":"2006","unstructured":"\u015avejdar, V.: On sequent calculi for intuitionistic propositional logic. Commentationes Mathematicae Universitatis Carolinae\u00a047(1), 159\u2013173 (2006)","journal-title":"Commentationes Mathematicae Universitatis Carolinae"},{"key":"9_CR15","volume-title":"The Collected Papers of Gerhard Gentzen. Studies in Logic and the foundations of Mathematics","author":"M.E. Szabo","year":"1969","unstructured":"Szabo, M.E.: The Collected Papers of Gerhard Gentzen. Studies in Logic and the foundations of Mathematics. North-Holland, Amsterdam (1969)"},{"issue":"3","key":"9_CR16","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1305\/ndjfl\/1039886520","volume":"37","author":"I. Urbas","year":"1996","unstructured":"Urbas, I.: Dual-intuitionistic logic. NDJFL\u00a037(3), 440\u2013451 (1996)","journal-title":"NDJFL"},{"key":"9_CR17","unstructured":"Uustalu, T.: Personal communication. via email (2004)"},{"key":"9_CR18","unstructured":"Uustalu, T.: Personal communication. via email (2006)"},{"key":"9_CR19","unstructured":"Uustalu, T., Pinto, L.: Days in logic \u201906 conference abstract (accessed on 27th October 2006), http:\/\/www.mat.uc.pt\/?kahle\/dl06\/tarmo-uustalu.pdf"},{"issue":"4","key":"9_CR20","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1023\/A:1004218110879","volume":"27","author":"F. Wolter","year":"1998","unstructured":"Wolter, F.: On logics with coimplication. JPL\u00a027(4), 353\u2013387 (1998)","journal-title":"JPL"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73099-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T00:14:06Z","timestamp":1684023246000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73099-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540730989","9783540730996"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73099-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}