{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:38:28Z","timestamp":1763642308570,"version":"3.37.3"},"reference-count":37,"publisher":"Oxford University Press (OUP)","issue":"1","funder":[{"name":"FCT","award":["UID\/MAT\/00013\/2013"],"award-info":[{"award-number":["UID\/MAT\/00013\/2013"]}]},{"DOI":"10.13039\/501100008530","name":"ERDF","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001837","name":"Estonian Science Foundation","doi-asserted-by":"crossref","award":["6940"],"award-info":[{"award-number":["6940"]}],"id":[{"id":"10.13039\/501100001837","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,2,1]]},"DOI":"10.1093\/logcom\/exx044","type":"journal-article","created":{"date-parts":[[2017,12,1]],"date-time":"2017-12-01T23:09:34Z","timestamp":1512169774000},"page":"165-202","source":"Crossref","is-referenced-by-count":8,"title":["A proof-theoretic study of bi-intuitionistic propositional sequent calculus"],"prefix":"10.1093","volume":"28","author":[{"given":"Lu\u00eds","family":"Pinto","sequence":"first","affiliation":[{"name":"Centro de Matem\u00e1tica, Universidade do Minho, Campus de Gualtar, Braga, Portugal"}]},{"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[{"name":"Institute of Cybernetics at Tallinn University of Technology, Tallinn, Estonia"}]}],"member":"286","published-online":{"date-parts":[[2018,2,1]]},"reference":[{"key":"key\n\t\t\t\t20180322034303_C1","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1093\/logcom\/14.4.473","article-title":"Towards a logic for pragmatics: assertions and conjectures","volume":"14","author":"Bellin","year":"2004","journal-title":"J. of Log. and Comput."},{"key":"key\n\t\t\t\t20180322034303_C2","doi-asserted-by":"crossref","DOI":"10.1093\/logcom\/exv036","article-title":"On an intuitionistic logic for pragmatics","volume-title":"J. of Log. and Comput","author":"Bellin"},{"volume-title":"Nested Sequents","year":"2010","author":"Br\u00fcnnler","key":"key\n\t\t\t\t20180322034303_C3"},{"key":"key\n\t\t\t\t20180322034303_C4","first-page":"90","article-title":"A cut-free sequent calculus for bi-intuitionistic logic","volume-title":"Proceedings of 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2007, Lect. Notes in Comput. Sci","author":"Buisman","year":"2007"},{"key":"key\n\t\t\t\t20180322034303_C5","doi-asserted-by":"crossref","first-page":"1245","DOI":"10.1007\/s11225-014-9566-z","article-title":"Hypersequent and display calculi\u2014a unified perspective","volume":"102","author":"Ciabattoni","year":"2014","journal-title":"Studia Logica"},{"key":"key\n\t\t\t\t20180322034303_C6","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/S0304-3975(99)00124-3","article-title":"Subtractive logic","volume":"254","author":"Crolard","year":"2001","journal-title":"Theor. Comput. Sci."},{"key":"key\n\t\t\t\t20180322034303_C7","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1093\/logcom\/14.4.529","article-title":"A formulae-as-types interpretation of subtractive logic","volume":"14","author":"Crolard","year":"2004","journal-title":"J. of Log. and Comput."},{"key":"key\n\t\t\t\t20180322034303_C8","doi-asserted-by":"crossref","unstructured":"P.\u2013L. Curien and H.Herbelin. The duality of computation. In Proceedings of 5th International Conference on Funct. Prog., ICFP \u201900, pp. 233--243. ACM Press, 2000.","DOI":"10.1145\/351240.351262"},{"key":"key\n\t\t\t\t20180322034303_C9","doi-asserted-by":"crossref","DOI":"10.1090\/mmono\/067","volume-title":"Mathematical Intuitionism: Introduction to Proof Theory","author":"Dragalin","year":", 1988"},{"key":"key\n\t\t\t\t20180322034303_C10","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","article-title":"Contraction-free sequent calculi for intuitionistic logic","volume":"57","author":"Dyckhoff","year":"1992","journal-title":"J. of Symb. Logic"},{"key":"key\n\t\t\t\t20180322034303_C11","first-page":"71","article-title":"Proof analysis in intermediate logics","volume-title":"Arch. of Math. Log","author":"Dyckhoff","year":"2012"},{"key":"key\n\t\t\t\t20180322034303_C12","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/j.apal.2011.09.004","article-title":"Prefixed tableaus and nested sequents","volume":"163","author":"Fitting","year":"2012","journal-title":"Ann. of Pure and Appl. Log."},{"key":"key\n\t\t\t\t20180322034303_C13","doi-asserted-by":"crossref","unstructured":"G. Gentzen . Investigations into logical deduction. In: M. E.Szabo, ed.,The Collected Papers of Gerhard Gentzen, pp. 68--131. North-Holland, 1969.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"key\n\t\t\t\t20180322034303_C14","first-page":"119","article-title":"The logic of contradiction","volume-title":"Zeitschr. f. math. Logik und Grundl. d. Math","author":"Goodman","year":"1977"},{"key":"key\n\t\t\t\t20180322034303_C15","doi-asserted-by":"crossref","unstructured":"R. Gor\u00e9 . Dual intuitionistic logic revisited. In R.Dyckhoff, ed., Proceedings of 9th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2000, Lect. Notes in Artif. Intell. 1847, pp. 263--267. Springer, 2000.","DOI":"10.1007\/10722086_21"},{"key":"key\n\t\t\t\t20180322034303_C16","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1093\/logcom\/exn067","article-title":"Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic","volume":"20","author":"Gor\u00e9","year":"2008","journal-title":"J. of Log. and Comput."},{"key":"key\n\t\t\t\t20180322034303_C17","unstructured":"R. Gor\u00e9 , L.Postniece and A.Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In C.Areces and R.Goldblatt, eds., Advances in Modal Logic 7, pp. 43--66. College Publications, 2008."},{"key":"key\n\t\t\t\t20180322034303_C18","unstructured":"R. Gor\u00e9 and R.Ramanayake. Labelled tree sequents, tree hypersequents and nested (deep) sequents. In T.Bolander, T.Bra\u00fcner, S.Ghilardi and L.Moss, eds., Advances in Modal Logic 9, pp. 279--299. College Publications, 2012."},{"volume-title":"Introduction to Metamathematics.","year":"1952","author":"Kleene","key":"key\n\t\t\t\t20180322034303_C19"},{"key":"key\n\t\t\t\t20180322034303_C20","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1017\/S175502031600040X","article-title":"Analytic cut and interpolation for bi-intuitionistic logic","volume":"10","author":"Kowalski","year":"2017","journal-title":"Rev. of Symb. Log"},{"key":"key\n\t\t\t\t20180322034303_C21","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/2528930","article-title":"A unified semantic framework for fully structural propositional sequent systems","volume":"14","author":"Lahav","year":"2013","journal-title":"ACM Trans. Comput. Log"},{"key":"key\n\t\t\t\t20180322034303_C22","first-page":"80","article-title":"Modal interpretation of Heyting\u2013Brouwer logic","volume-title":"Bull. of Sect. of Logic","author":"\u0141ukowski","year":"1996"},{"key":"key\n\t\t\t\t20180322034303_C23","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1017\/S0027763000018055","article-title":"Eine Darstellung der intuitionistischen Logik in der klassischen","volume":"3","author":"Maehara","year":"1954","journal-title":"Nagoya Math. J.,"},{"journal-title":"Caracteriza\u00e7\u00f5es sem\u00e2nticas e dedutivas da l\u00f3gica bi-intuicionista","year":"2006","author":"Monteiro","key":"key\n\t\t\t\t20180322034303_C24"},{"key":"key\n\t\t\t\t20180322034303_C25","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","article-title":"Proof analysis in modal logic","volume":"34","author":"Negri","year":"2005","journal-title":"J. of Philos. Logic"},{"key":"key\n\t\t\t\t20180322034303_C26","doi-asserted-by":"crossref","unstructured":"S. Negri . Proof analysis in non-classical logics. In C.Dimitracopoulos, L.Newelski, D.Normann and J.Steel, eds., Logic Colloquium 2005, Lect. Notes in Logic 28, pp. 107--128. Cambridge University Press, 2007.","DOI":"10.1017\/CBO9780511546464.010"},{"key":"key\n\t\t\t\t20180322034303_C27","first-page":"295","article-title":"Proof search and counter-model construction for bi-intuitionistic propositional logic with labeled sequents","volume-title":"Proceedings of 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009, Lect. Notes in Artif. Intell.","author":"Pinto","year":"2009"},{"key":"key\n\t\t\t\t20180322034303_C28","first-page":"55","article-title":"Relating sequent calculi for bi-intuitionistic propositional logic","author":"Pinto","year":"2011","journal-title":"Proceedings of 3rd Workshop on Classical Logic and Computation, CLaC 2010, Electronic Proceedings in Theoretical Computer Science"},{"key":"key\n\t\t\t\t20180322034303_C29","first-page":"320","article-title":"Deep inference in bi-intuitionistic logic","volume-title":"Proceedings of 16th International Workshop on Logic, Language, Information and Computation, WoLLiC 2009 (Tokyo, June 2009), Lect. Notes in Artif. Intell.","author":"Postniece","year":"2009"},{"volume-title":"Proof Theory and Proof Search of Bi-intuitionistic and Tense Logic","year":"2010","author":"Postniece","key":"key\n\t\t\t\t20180322034303_C30"},{"key":"key\n\t\t\t\t20180322034303_C31","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/BF02120864","article-title":"A formalization of the propositional calculus of H-B logic","volume":"33","author":"Rauszer","year":"1974","journal-title":"Studia Logica"},{"key":"key\n\t\t\t\t20180322034303_C32","doi-asserted-by":"crossref","first-page":"219","DOI":"10.4064\/fm-83-3-219-249","article-title":"Semi-boolean algebras and their applications to intuitionistic logic with dual operators","volume":"83","author":"Rauszer","year":"1974","journal-title":"Fund. Math"},{"key":"key\n\t\t\t\t20180322034303_C33","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BF02121115","article-title":"Applications of Kripke models to Heyting\u2013Brouwer logic","volume":"36","author":"Rauszer","year":"1977","journal-title":"Studia Logica"},{"key":"key\n\t\t\t\t20180322034303_C34","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/j.entcs.2009.02.031","article-title":"Intuitionistic letcc via labeled deduction","volume":"231","author":"Reed","year":"2009","journal-title":"Electron. Notes in Theor. Comput. Sci.,"},{"volume-title":"Extending intuitionistic logic with subtraction","year":"1997","author":"Restall","key":"key\n\t\t\t\t20180322034303_C35"},{"volume-title":"On the Relationship between Hypersequent Calculi and Labelled Sequent Calculi for Intermediate Logics with Geometric Kripke Semantics","year":"2010","author":"Rothenberg","key":"key\n\t\t\t\t20180322034303_C36"},{"key":"key\n\t\t\t\t20180322034303_C37","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1093\/logcom\/ext035","article-title":"Falsification, natural deduction and bi-intuitionistic logic","volume":"26","author":"Wansing","year":"2016","journal-title":"J. of Log. and Comput."}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/28\/1\/165\/23747814\/exx044.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T04:27:57Z","timestamp":1570422477000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/28\/1\/165\/4807375"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,1]]},"references-count":37,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2018,2,1]]},"published-print":{"date-parts":[[2018,2,1]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exx044","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2018,2]]},"published":{"date-parts":[[2018,2,1]]}}}