{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T17:31:29Z","timestamp":1777915889547,"version":"3.51.4"},"reference-count":111,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2014,7,4]],"date-time":"2014-07-04T00:00:00Z","timestamp":1404432000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2014,12]]},"DOI":"10.1007\/s11225-014-9566-z","type":"journal-article","created":{"date-parts":[[2014,7,3]],"date-time":"2014-07-03T05:57:01Z","timestamp":1404367021000},"page":"1245-1294","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Hypersequent and Display Calculi \u2013 a Unified Perspective"],"prefix":"10.1007","volume":"102","author":[{"given":"Agata","family":"Ciabattoni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Revantha","family":"Ramanayake","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heinrich","family":"Wansing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,7,4]]},"reference":[{"issue":"3","key":"9566_CR1","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"Andreoli J.-M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Logic Comput."},{"issue":"4","key":"9566_CR2","doi-asserted-by":"crossref","first-page":"939","DOI":"10.2307\/2273828","volume":"52","author":"A. Avron","year":"1987","unstructured":"Avron A.: A constructive analysis of RM. J. of Symbolic Logic 52(4), 939\u2013951 (1987)","journal-title":"J. of Symbolic Logic"},{"issue":"3-4","key":"9566_CR3","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BF01531058","volume":"4","author":"A. Avron","year":"1991","unstructured":"Avron A.: Hypersequents, logical consequence and intermediate logics for concurrency. Annals of Mathematics and Artificial Intelligence 4(3-4), 225\u2013248 (1991)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9566_CR4","doi-asserted-by":"crossref","unstructured":"Avron, A., The method of hypersequents in the proof theory of propositional nonclassical logics. In Logic: from foundations to applications (Staffordshire, 1993), Oxford Sci. Publ., Oxford Univ. Press, New York, 1996, pp. 1\u201332.","DOI":"10.1093\/oso\/9780198538622.003.0001"},{"key":"9566_CR5","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1093\/logcom\/exi001","volume":"15","author":"A. Avron","year":"2005","unstructured":"Avron A., Lev I.: Non-deterministic multi-valued structures. J. Logic Comput. 15, 241\u2013261 (2005)","journal-title":"J. Logic Comput."},{"key":"9566_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/logcom\/13.6.835","volume":"13","author":"M. Baaz","year":"2003","unstructured":"Baaz M., Ciabattoni A., Ferm\u00fcller C.G.: Hypersequent calculi for G\u00f6del logics: A survey. J. Logic Comput. 13, 1\u201327 (2003)","journal-title":"J. Logic Comput."},{"issue":"4","key":"9566_CR7","doi-asserted-by":"crossref","first-page":"315","DOI":"10.3233\/FUN-2004-59401","volume":"59","author":"M. Baaz","year":"2004","unstructured":"Baaz M., Ciabattoni A., Montagna F.: Analytic calculi for monoidal t-norm based logic. Fundamenta Informaticae 59(4), 315\u2013332 (2004)","journal-title":"Fundamenta Informaticae"},{"key":"9566_CR8","unstructured":"Baaz, M., and C. G. Ferm\u00fcller, Analytic calculi for projective logics. In Tableaux \u201999. LNAI, vol. 1617. Springer, 1999, pp. 36\u201350."},{"issue":"1","key":"9566_CR9","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1005022012721","volume":"61","author":"M. Baaz","year":"1998","unstructured":"Baaz M., Ferm\u00fcller C.G., Salzer G., Zach R.: Labeled calculi and finite-valued logics. Studia Logica 61(1), 7\u201333 (1998)","journal-title":"Studia Logica"},{"key":"9566_CR10","first-page":"333","volume":"29","author":"M. Baaz","year":"1994","unstructured":"Baaz M., Ferm\u00fcller C.G., Zach R.: Elimination of cuts in first-order many-valued logics. J. of Inf. Proc. and Cybernetics 29, 333\u2013355 (1994)","journal-title":"J. of Inf. Proc. and Cybernetics"},{"key":"9566_CR11","doi-asserted-by":"crossref","unstructured":"Baaz, M., O. Lahav, and A. Zamansky, Finite-valued semantics for canonical labelled calculi. J. of Automated Reasoning, 2013.","DOI":"10.1007\/s10817-013-9273-x"},{"key":"9566_CR12","doi-asserted-by":"crossref","unstructured":"Baaz, M., and R. Zach, Hypersequents and the proof theory of intuitionistic fuzzy logic. In CSL\u201900. LNCS. Springer, 2000, pp. 187\u2013201.","DOI":"10.1007\/3-540-44622-2_12"},{"key":"9566_CR13","unstructured":"Baldi, P., A. Ciabattoni, and L. Spendier, Standard completeness for extensions of MTL: an automated approach. In WOLLIC 2012, vol. 7456 of LNCS. Springer, 2012, pp. 154\u2013167."},{"key":"9566_CR14","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1093\/analys\/22.6.130","volume":"22","author":"N.D. Belnap Jr.","year":"1962","unstructured":"Belnap N.D. Jr.: Tonk, plonk and plik. Analysis 22, 130\u2013134 (1962)","journal-title":"Analysis"},{"issue":"4","key":"9566_CR15","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"N.D. Belnap Jr.","year":"1982","unstructured":"Belnap N.D. Jr.: Display logic. J. Philos. Logic 11(4), 375\u2013417 (1982)","journal-title":"J. Philos. Logic"},{"key":"9566_CR16","doi-asserted-by":"crossref","unstructured":"Belnap, N. D., Jr., The display problem. In H. Wansing, (ed.), Proof Theory of Modal Logic. Kluwer, Dordrecht, 1996, pp. 79\u201392.","DOI":"10.1007\/978-94-017-2798-3_6"},{"key":"9566_CR17","doi-asserted-by":"crossref","unstructured":"Blackburn, P., M. de Rijke, and I. Venema, Modal logic, vol. 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2001.","DOI":"10.1017\/CBO9781107050884"},{"issue":"6","key":"9566_CR18","doi-asserted-by":"crossref","first-page":"1223","DOI":"10.1007\/s11225-012-9449-0","volume":"100","author":"J. Brotherston","year":"2012","unstructured":"Brotherston J.: Bunched logics displayed. Studia Logica 100(6), 1223\u20131254 (2012)","journal-title":"Studia Logica"},{"key":"9566_CR19","unstructured":"Brotherston, J., and R. Gor\u00e9, Craig interpolation in displayable logics. In Tableaux 2011, vol. 6793 of LNCS. Springer, 2011, pp. 88\u2013103."},{"key":"9566_CR20","unstructured":"Br\u00fcnnler, K., Deep sequent systems for modal logic. In Advances in modal logic. Vol. 6. Coll. Publ., London, 2006, pp. 107\u2013119."},{"key":"9566_CR21","unstructured":"Ciabattoni, A., Automated generation of analytic calculi for logics with linearity. In CSL04. LNCS, vol. 3210. Springer, 2004, pp. 503\u2013517."},{"key":"9566_CR22","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., A proof-theoretical investigation of global intuitionistic (fuzzy) logic. Archive of mathematical Logic 44:435\u2013457, 2005.","DOI":"10.1007\/s00153-004-0265-8"},{"key":"9566_CR23","unstructured":"Ciabattoni, A., C. G. Ferm\u00fcller, and G. Metcalfe, Uniform rules and dialogue games for fuzzy logics. In LPAR 2004. LNCS, vol. 3452, 2004, pp. 496\u2013510."},{"key":"9566_CR24","unstructured":"Ciabattoni, A., and M. Ferrari, Hypertableau and path-hypertableau calculi for some families of intermediate logics. In Tableaux 2000. LNAI, vol. 1847, 2000, pp. 160\u2013175."},{"issue":"4","key":"9566_CR25","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/s005000050047","volume":"2","author":"A. Ciabattoni","year":"1999","unstructured":"Ciabattoni A., Gabbay D., Olivetti N.: Cut-free proof systems for logics of weak excluded middle. Soft Computing 2(4), 147\u2013156 (1999)","journal-title":"Soft Computing"},{"key":"9566_CR26","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., N. Galatos, and K. Terui, From axioms to analytic rules in nonclassical logics. In LICS 2008, 2008, pp. 229\u2013240.","DOI":"10.1109\/LICS.2008.39"},{"key":"9566_CR27","unstructured":"Ciabattoni, A., N. Galatos, and K. Terui. Algebraic proof theory: hypersequents and hypercompletions. submitted. 2014."},{"key":"9566_CR28","unstructured":"Ciabattoni, A., P. Maffezioli, and L. Spendier, Hypersequent and labelled calculi for intermediate logics. In Tableaux 2013. LNCS, vol. 8123. Springer, 2013, pp. 81\u201396."},{"key":"9566_CR29","unstructured":"Ciabattoni, A., and G. Metcalfe, Bounded \u0141ukasiewicz logics. In Tableaux 2003. LNCS, vol. 2796. Springer, 2003, pp. 32\u201347."},{"issue":"2-3","key":"9566_CR30","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1016\/j.tcs.2008.05.019","volume":"403","author":"A. Ciabattoni","year":"2008","unstructured":"Ciabattoni A., Metcalfe G.: Density elimination. Theor. Comput. Sci. 403(2-3), 328\u2013346 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"9566_CR31","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1016\/j.fss.2009.09.001","volume":"161","author":"A. Ciabattoni","year":"2010","unstructured":"Ciabattoni A., Metcalfe G., Montagna F.: Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions. Fuzzy Sets and Systems 161(3), 369\u2013389 (2010)","journal-title":"Fuzzy Sets and Systems"},{"key":"9566_CR32","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/j.tcs.2013.02.003","volume":"480","author":"A. Ciabattoni","year":"2013","unstructured":"Ciabattoni A., Montagna F.: Proof theory for locally finite many-valued logics: Semi-projective logics. Theor. Comput. Sci. 480, 26\u201342 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"9566_CR33","unstructured":"Ciabattoni, A., and R. Ramanayake, Structural rule extensions of display calculi: a general recipe. In WOLLIC 2013, vol. 8071 of LNCS. Springer, 2013, pp. 81\u201395."},{"key":"9566_CR34","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., L. Strassburger, and K. Terui, Expanding the realm of systematic proof theory. In CSL 2009. LNCS. Springer, 2009, pp. 163\u2013178.","DOI":"10.1007\/978-3-642-04027-6_14"},{"key":"9566_CR35","unstructured":"Clouston, R., R. Gor\u00e9, and A. Tiu, Annotation-free sequent calculi for full intuitionistic linear logic. In CSL 2013, LNCS. Springer, 2013, pp. 197\u2013214."},{"issue":"3","key":"9566_CR36","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1016\/j.apal.2011.10.004","volume":"163","author":"W. Conradie","year":"2012","unstructured":"Conradie W., Palmigiano A.: Algorithmic correspondence and canonicity for distributive modal logic. Annals of Pure and Applied Logic 163(3), 338\u2013376 (2012)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"4","key":"9566_CR37","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/malq.19890350402","volume":"35","author":"G. Corsi","year":"1989","unstructured":"Corsi G.: A cut-free calculus for Dummett\u2019s LC quantified. Mathematical Logic Quarterly 35(4), 289\u2013301 (1989)","journal-title":"Mathematical Logic Quarterly"},{"key":"9566_CR38","unstructured":"Dawson, J. E., and R. Gor\u00e9, Formalised cut admissibility for display logic. In Theorem proving in higher order logics, vol. 2410 of LNCS. Springer, Berlin, 2002, pp. 131\u2013147."},{"key":"9566_CR39","doi-asserted-by":"crossref","unstructured":"Dawson, J. E., and R. Gor\u00e9, A new machine-checked proof of strong normalisation for display logic. In Electronic Notes in Theoretical Computer Science. Elsevier, 2002.","DOI":"10.1016\/S1571-0661(04)81004-1"},{"issue":"6","key":"9566_CR40","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1093\/logcom\/12.6.993","volume":"12","author":"S. Demri","year":"2002","unstructured":"Demri S., Gor\u00e9 R.: Display calculi for nominal tense logics. J. Logic Comput. 12(6), 993\u20131016 (2002)","journal-title":"J. Logic Comput."},{"key":"9566_CR41","unstructured":"Dummett, M., Frege: Philosophy of Language. Harper & Row, New York, 1973."},{"key":"9566_CR42","unstructured":"Dunn, J. M., A \u2018Gentzen\u2019 system for positive relevant implication. J. of Symbolic Logic 38:356-357, 1974. (Abstract)."},{"key":"9566_CR43","volume-title":"A mathematical introduction to logic","author":"H. Enderton","year":"1972","unstructured":"Enderton H.: A mathematical introduction to logic. Academic Press, New York (1972)"},{"key":"9566_CR44","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/S0165-0114(01)00098-7","volume":"124","author":"F. Esteva","year":"2001","unstructured":"Esteva F., Godo L.: Monoidal t-norm based logic: towards a logic for leftcontinuous t-norms. Fuzzy Sets and Systems 124, 271\u2013288 (2001)","journal-title":"Fuzzy Sets and Systems"},{"key":"9566_CR45","doi-asserted-by":"crossref","unstructured":"Fitting, M., Proof methods for modal and intuitionistic logics, vol. 169 of Synthese Library. D. Reidel Publishing Co., Dordrecht, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"9566_CR46","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Labelled Deductive Systems, vol. 1\u2014Foundations. Oxford University Press, 1996.","DOI":"10.1093\/oso\/9780198538332.003.0001"},{"key":"9566_CR47","unstructured":"Galatos, N., P. Jipsen, T. Kowalski, and H. Ono, Residuated lattices: an algebraic glimpse at substructural logics, vol. 151 of Studies in Logic and the Foundations of Mathematics. Elsevier B. V., Amsterdam, 2007."},{"key":"9566_CR48","unstructured":"Gentzen, G., Untersuchungen \u00fcber das logische schlie\u00dfen. Mathematische Zeitschrift 39:176\u2013210, 405\u2013431, 1934\/35. English translation in: American Philosophical Quarterly 1 (1964), 288\u2013306 and American Philosophical Quarterly 2 (1965), 204\u2013218, as well as in: The Collected Papers of Gerhard Gentzen, (ed. M. E. Szabo), Amsterdam, North Holland (1969), pp. 68\u2013131."},{"key":"9566_CR49","unstructured":"Goldblatt, R., Topoi. The Categorical Analysis of Logic. North-Holland, Amsterdam, 1979."},{"key":"9566_CR50","unstructured":"Gor\u00e9, R., Gaggles, Gentzen and Galois: how to display your favourite substructural logic. Log. J. IGPL 6(5):669\u2013694, 1998."},{"issue":"3","key":"9566_CR51","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1093\/jigpal\/6.3.451","volume":"6","author":"R. Gor\u00e9","year":"1998","unstructured":"Gor\u00e9 R.: Substructural logics on display. Log. J. IGPL 6(3), 451\u2013504 (1998)","journal-title":"Log. J. IGPL"},{"key":"9566_CR52","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R., L. Postniece, and A. Tiu, On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Log. Methods Comput. Sci. 7(2):2:8, 38, 2011.","DOI":"10.2168\/LMCS-7(2:8)2011"},{"key":"9566_CR53","unstructured":"Gor\u00e9, R., and R. Ramanayake, Labelled tree sequents, tree hypersequents and nested (deep) sequents. In Advances in modal logic. Volume 9. College Publications, London, 2012."},{"issue":"4","key":"9566_CR54","doi-asserted-by":"crossref","first-page":"767","DOI":"10.1093\/logcom\/exm026","volume":"17","author":"R. Gor\u00e9","year":"2007","unstructured":"Gor\u00e9 R., Tiu A.: Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5. J. Logic Comput. 17(4), 767\u2013794 (2007)","journal-title":"J. Logic Comput."},{"key":"9566_CR55","unstructured":"Grazl, N., Sequent calculi for multi-modal logic with interaction. In D. Grossi, O. Roy, and H. Huang, (eds.), Logic, Rationality, and Interaction, vol. 8196 of Lecture Notes in Computer Science Springer Berlin Heidelberg, 2013, pp. 124\u2013134."},{"key":"9566_CR56","unstructured":"Guglielmi, A., Deep inference. http:\/\/alessio.guglielmi.name\/res\/cos\/index.html . Accessed: 2013-10-14."},{"key":"9566_CR57","doi-asserted-by":"crossref","unstructured":"Guglielmi, A., A system of interaction and structure. TOCL, 8(1), 2007.","DOI":"10.1145\/1182613.1182614"},{"key":"9566_CR58","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2307\/2025471","volume":"76","author":"I. Hacking","year":"1979","unstructured":"Hacking I.: What is logic?. J. Phil. 76, 285\u2013319 (1979)","journal-title":"J. Phil."},{"key":"9566_CR59","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R., Automated Deduction in Multiple-valued Logics. Oxford University Press, 1993.","DOI":"10.1093\/oso\/9780198539896.001.0001"},{"key":"9566_CR60","doi-asserted-by":"crossref","unstructured":"H\u00e1jek, P., Metamathematics of Fuzzy Logic. Kluwer, Dordrecht, 1998.","DOI":"10.1007\/978-94-011-5300-3"},{"key":"9566_CR61","unstructured":"Hor\u010d\u00edk, R., Algebraic semantics: Semilinear FL-algebras. In Handbook of Mathematical Fuzzy Logic, vol 1, vol. 37 of Studies in Logic, Mathematical Logic and Foundations, pp. 175\u2013214. College Publications, London, 2011."},{"key":"9566_CR62","unstructured":"Iemhoff, R., and G. Metcalfe, Hypersequent systems for the admissible rules of modal and intermediate logics. In LNCS, vol. 5407. Springer, 2009, pp. 230\u2013245."},{"issue":"1-2","key":"9566_CR63","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/j.apal.2008.10.011","volume":"159","author":"R. Iemhoff","year":"2009","unstructured":"Iemhoff R., Metcalfe G.: Proof theory for admissible rules. Annals of Pure and Applied Logic 159(1-2), 171\u2013186 (2009)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1-2","key":"9566_CR64","first-page":"89","volume":"41","author":"A. Indrzejczak","year":"2012","unstructured":"Indrzejczak A.: Cut-free hypersequent calculus for S4.3. Bull. Sect. Logic Univ. \u0141\u00f3d\u017a 41(1-2), 89\u2013104 (2012)","journal-title":"Bull. Sect. Logic Univ. \u0141\u00f3d\u017a"},{"issue":"1","key":"9566_CR65","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/BF01053026","volume":"53","author":"R. Kashima","year":"1994","unstructured":"Kashima R.: Cut-free sequent calculi for some tense logics. Studia Logica 53(1), 119\u2013135 (1994)","journal-title":"Studia Logica"},{"key":"9566_CR66","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0304-3975(01)00320-6","volume":"286","author":"B. Konikowska","year":"2002","unstructured":"Konikowska B.: Rasiowa-Sikorski Deduction Systems in CS applications. Theoretical Computer Science 286, 323\u2013366 (2002)","journal-title":"Theoretical Computer Science"},{"key":"9566_CR67","doi-asserted-by":"crossref","unstructured":"Kracht, M., Power and weakness of the modal display calculus. In Proof theory of modal logic (Hamburg, 1993), vol. 2 of Appl. Log. Ser.. Kluwer Acad. Publ., Dordrecht, 1996, pp. 93\u2013121.","DOI":"10.1007\/978-94-017-2798-3_7"},{"key":"9566_CR68","unstructured":"Kurz, A., G. Greco, and A. Palmigiani, Dynamic epistemic logic displayed. In Logic, Rationality, and Interaction, vol. 8196 of LNCS. Springer, 2013, pp. 135\u2013148."},{"key":"9566_CR69","doi-asserted-by":"crossref","unstructured":"Lahav, O., From frame properties to hypersequent rules in modal logics. In LICS 2013, IEEE, 2013, pp. 408\u2013417.","DOI":"10.1109\/LICS.2013.47"},{"key":"9566_CR70","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00370318","volume":"39","author":"D. Leivant","year":"1980","unstructured":"Leivant D.: Quantifiers as modal operators. Studia Logica 39, 145\u2013158 (1980)","journal-title":"Studia Logica"},{"key":"9566_CR71","unstructured":"Lellmann, B., and D. Pattinson, Correspondence between modal Hilbert axioms and sequent rules with an application to S5. In Tableaux 2013. LNCS, vol. 8123. Springer, pp. 219\u2013233, 2013."},{"issue":"3","key":"9566_CR72","doi-asserted-by":"crossref","first-page":"834","DOI":"10.2178\/jsl\/1191333844","volume":"72","author":"G. Metcalfe","year":"2007","unstructured":"Metcalfe G., Montagna F.: Substructural fuzzy logics. J. of Symbolic Logic 72(3), 834\u2013864 (2007)","journal-title":"J. of Symbolic Logic"},{"issue":"2","key":"9566_CR73","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-7(2:10)2011","volume":"7","author":"G. Metcalfe","year":"2011","unstructured":"Metcalfe G., Olivetti N.: Towards a proof theory of G\u00f6del modal logics. Logical Methods in Computer Science 7(2), 1\u201327 (2011)","journal-title":"Logical Methods in Computer Science"},{"issue":"7","key":"9566_CR74","doi-asserted-by":"crossref","first-page":"859","DOI":"10.1007\/s00153-004-0225-3","volume":"43","author":"G. Metcalfe","year":"2004","unstructured":"Metcalfe G., Olivetti N., Gabbay D.: Analytic proof calculi for product logics. Archive for Mathematical Logic 43(7), 859\u2013889 (2004)","journal-title":"Archive for Mathematical Logic"},{"issue":"3","key":"9566_CR75","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1145\/1071596.1071600","volume":"6","author":"G. Metcalfe","year":"2005","unstructured":"Metcalfe G., Olivetti N., Gabbay D.: Sequent and hypersequent calculi for abelian and \u0141ukasiewicz logics. ACM Transactions on Computational Logic 6(3), 578\u2013613 (2005)","journal-title":"ACM Transactions on Computational Logic"},{"key":"9566_CR76","doi-asserted-by":"crossref","unstructured":"Metcalfe, G., N. Olivetti, and D. Gabbay, Proof Theory for Fuzzy Logics, vol. 39 of Springer Series in Applied Logic. Springer, 2009.","DOI":"10.1007\/978-1-4020-9409-5"},{"key":"9566_CR77","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/BF01084083","volume":"6","author":"G. Mints","year":"1976","unstructured":"Mints G.: Cut-elimination theorem in relevant logics. The Journal of Soviet Mathematics 6, 422\u2013428 (1976)","journal-title":"The Journal of Soviet Mathematics"},{"issue":"5-6","key":"9566_CR78","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-6), 507\u2013544 (2005)","journal-title":"J. Philos. Logic"},{"key":"9566_CR79","doi-asserted-by":"crossref","unstructured":"Paoli, F., Substructural Logics: A Primer. Kluwer Academic Publ. Dordrecht, 2002.","DOI":"10.1007\/978-94-017-3179-9"},{"key":"9566_CR80","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1080\/00048400701728574","volume":"85","author":"F. Paoli","year":"2007","unstructured":"Paoli F.: Implicational paradoxes and the meaning of logical constants. Australasian Journal of Philosophy 85, 553\u2013579 (2007)","journal-title":"Australasian Journal of Philosophy"},{"issue":"1","key":"9566_CR81","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S1755020308080040","volume":"1","author":"F. Poggiolesi","year":"2008","unstructured":"Poggiolesi F.: A cut-free simple sequent calculus for modal logic S5. The Review of Symbolic Logic 1(1), 3\u201315 (2008)","journal-title":"The Review of Symbolic Logic"},{"key":"9566_CR82","doi-asserted-by":"crossref","unstructured":"Poggiolesi, F., Gentzen Calculi for Modal Propositional Logic. Trends in Logic, Springer, 2010.","DOI":"10.1007\/978-90-481-9670-8"},{"key":"9566_CR83","doi-asserted-by":"crossref","unstructured":"Poggiolesi, F., and G. Restall, Interpreting and applying proof theories for modal logic. In G. Restall and G. Russell, (eds.), New Waves in Philosophical Logic. Palgrave Macmillan, Basingstoke, 2012, pp. 39\u201362.","DOI":"10.1057\/9781137003720.0007"},{"key":"9566_CR84","unstructured":"Pottinger, G., Uniform, cut-free formulations of T, S4 and S5 (abstract). J. of Symbolic Logic 48(3):900, 1983."},{"key":"9566_CR85","unstructured":"Prawitz, D., Natural Deduction. A Proof-theoretical Study. Almqvist and Wiksell, Stockholm, 1965."},{"key":"9566_CR86","doi-asserted-by":"crossref","unstructured":"Ramanayake, R., Embedding the hypersequent calculus in the display calculus. submitted. 2013.","DOI":"10.1093\/logcom\/exu061"},{"key":"9566_CR87","doi-asserted-by":"crossref","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 \u2013 B logic. Studia Logica 33, 23\u201334 (1974)","journal-title":"Studia Logica"},{"key":"9566_CR88","unstructured":"Restall, G., Display logic and gaggle theory. Rep. Math. Logic (29):133\u2013146, 1995."},{"issue":"2","key":"9566_CR89","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1023\/A:1017998605966","volume":"27","author":"G. Restall","year":"1998","unstructured":"Restall G.: Displaying and deciding substructural logics. I. Logics with contraposition. J. Philos. Logic 27(2), 179\u2013216 (1998)","journal-title":"J. Philos. Logic"},{"key":"9566_CR90","volume-title":"An Introduction to Substructural Logics","author":"G. Restall","year":"1999","unstructured":"Restall G.: An Introduction to Substructural Logics. Routledge, London (1999)"},{"issue":"11","key":"9566_CR91","doi-asserted-by":"crossref","first-page":"1611","DOI":"10.1016\/j.apal.2011.12.012","volume":"163","author":"G. Restall","year":"2012","unstructured":"Restall G.: A cut-free sequent system for two-dimensional modal logic, and why it matters. Ann. Pure Appl. Logic 163(11), 1611\u20131623 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9566_CR92","doi-asserted-by":"crossref","unstructured":"Rousseau, G., Sequents in many valued logic I, and II. Fundamenta Mathematic\u00e6 LX, LXVII:23\u201333, 125\u2013131, 1967, 1970.","DOI":"10.4064\/fm-67-1-125-131"},{"key":"9566_CR93","unstructured":"Schroeder-Heister, P., Sequent calculi and bidirectional natural deduction: On the proper basis of proof-theoretic semantics. In M. Peli\u0161, (ed.), Logica Yearbook 2008. College Publications, London, 2008, pp. 237\u2013251."},{"key":"9566_CR94","unstructured":"Schroeder-Heister, P., Proof-theoretic semantics. The Stanford Encyclopedia of Philosophy, E. N. Zalta (ed.), Spring 2013 Edition."},{"key":"9566_CR95","unstructured":"Standefer, S., Philosophical aspects of display logic. In M. Peli\u0161, (ed.), Logica Yearbook 2009. College Publications, London, 2009, pp. 283\u2013295."},{"key":"9566_CR96","unstructured":"Takeuti, G., Proof theory, vol. 81 of Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1987."},{"issue":"3","key":"9566_CR97","doi-asserted-by":"crossref","first-page":"851","DOI":"10.2307\/2274139","volume":"49","author":"G. Takeuti","year":"1984","unstructured":"Takeuti G., Titani T.: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory. J. of Symbolic Logic 49(3), 851\u2013866 (1984)","journal-title":"J. of Symbolic Logic"},{"key":"9566_CR98","doi-asserted-by":"crossref","unstructured":"Tiu, A., A system of interaction and structure. II. The need for deep inference. Log. Methods Comput. Sci. 2(2):2:4, 24, 2006.","DOI":"10.2168\/LMCS-2(2:4)2006"},{"key":"9566_CR99","doi-asserted-by":"crossref","unstructured":"Tiu, A., A hypersequent system for G\u00f6del-Dummett logic with non-constant domains. In Tableaux 2011. LNAI, pp. 248\u2013262. Springer, 2011.","DOI":"10.1007\/978-3-642-22119-4_20"},{"key":"9566_CR100","unstructured":"Troelstra, A. S., and H. Schwichtenberg, Basic proof theory, vol. 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, second edition, 2000."},{"key":"9566_CR101","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1093\/jigpal\/5.2.259","volume":"5","author":"J. Benthem van","year":"1997","unstructured":"van Benthem J.: Modal foundations of predicate logic. Log. J. IGPL 5, 259\u2013286 (1997)","journal-title":"Log. J. IGPL"},{"key":"9566_CR102","doi-asserted-by":"crossref","unstructured":"Vigan\u00f2, L., Labelled non-classical logics. Kluwer Academic Publishers, Dordrecht, 2000. With a foreword by Dov M. Gabbay.","DOI":"10.1007\/978-1-4757-3208-5"},{"issue":"2","key":"9566_CR103","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1093\/logcom\/4.2.125","volume":"4","author":"H. Wansing","year":"1994","unstructured":"Wansing H.: Sequent calculi for normal modal propositional logics. J. Logic Comput. 4(2), 125\u2013142 (1994)","journal-title":"J. Logic Comput."},{"key":"9566_CR104","doi-asserted-by":"crossref","first-page":"719","DOI":"10.1093\/logcom\/7.6.719","volume":"7","author":"H. Wansing","year":"1997","unstructured":"Wansing H.: Modal tableaux based on residuation. J. Logic Comput. (7, 719\u2013731 (1997)","journal-title":"J. Logic Comput. ("},{"key":"9566_CR105","doi-asserted-by":"crossref","unstructured":"Wansing, H., Displaying Modal Logic. Springer, Trends in Logic, 1998.","DOI":"10.1007\/978-94-017-1280-4"},{"issue":"5","key":"9566_CR106","doi-asserted-by":"crossref","first-page":"719","DOI":"10.1093\/jigpal\/6.5.719","volume":"6","author":"H. Wansing","year":"1998","unstructured":"Wansing H.: Translation of hypersequents into display sequents. Log. J. IGPL 6(5), 719\u2013733 (1998)","journal-title":"Log. J. IGPL"},{"issue":"1","key":"9566_CR107","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1023\/A:1005125717300","volume":"62","author":"H. Wansing","year":"1999","unstructured":"Wansing H.: Predicate logics on display. Studia Logica 62(1), 49\u201375 (1999)","journal-title":"Studia Logica"},{"key":"9566_CR108","doi-asserted-by":"crossref","unstructured":"Wansing, H., Sequent systems for modal logics. In D. Gabbay and F. Guenthner, (eds.), Handbook of Philosophical Logic, vol. 8. Kluwer, 2002, pp. 61\u2013145.","DOI":"10.1007\/978-94-010-0387-2_2"},{"issue":"2-3","key":"9566_CR109","doi-asserted-by":"crossref","first-page":"341","DOI":"10.3166\/jancl.18.341-364","volume":"18","author":"H. Wansing","year":"2008","unstructured":"Wansing H.: Constructive negation, implication, and co-implication. J. Appl. Non-Classical Logics 18(2-3), 341\u2013364 (2008)","journal-title":"J. Appl. Non-Classical Logics"},{"key":"9566_CR110","doi-asserted-by":"crossref","unstructured":"Wansing, H., Prawitz, proofs, and meaning. In H. Wansing (ed.), Dag Prawitz on proofs and meaning. Springer, to appear 2014.","DOI":"10.1007\/978-3-319-11041-7"},{"issue":"4","key":"9566_CR111","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1023\/A:1004218110879","volume":"27","author":"F. Wolter","year":"1998","unstructured":"Wolter F.: On logics with coimplication. J. Philos. Logic 27(4), 353\u2013387 (1998)","journal-title":"J. Philos. Logic"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-014-9566-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-014-9566-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-014-9566-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T17:10:26Z","timestamp":1746292226000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-014-9566-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,4]]},"references-count":111,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["9566"],"URL":"https:\/\/doi.org\/10.1007\/s11225-014-9566-z","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7,4]]}}}