{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:30Z","timestamp":1747173450000,"version":"3.40.5"},"reference-count":43,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2022,11,23]],"date-time":"2022-11-23T00:00:00Z","timestamp":1669161600000},"content-version":"unspecified","delay-in-days":53,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The proof theory of the constructive modal logic <jats:italic>S<\/jats:italic>4 (hereafter <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000378_inline1.png\"\/><jats:tex-math>\n$\\mathsf{CS4}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>) has been settled since the beginning of this century by means of either standard natural deduction and sequent calculi or by the reconstruction of modal logic through hypothetical and categorical judgments \u00e0 la Martin-L\u00f6f, an approach carried out by using a special kind of sequents, which keeps two separated contexts representing ordinary and enhanced hypotheses, intuitively interpreted as true and valid assumptions. These so-called dual-context sequents, originated in linear logic, are used to define a natural deduction system handling judgments of validity, truth, and possibility, resulting in a formalism equivalent to an axiomatic system for <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000378_inline2.png\"\/><jats:tex-math>\n$\\mathsf{CS4}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. However, this proof-theoretical study of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000378_inline3.png\"\/><jats:tex-math>\n$\\mathsf{CS4}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> lacks, to the best of our knowledge, its third fundamental constituent, namely a sequent calculus. In this paper, we define such a dual-context formalism, called <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000378_inline4.png\"\/><jats:tex-math>\n${\\bf DG_{CS4}}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, and provide detailed proofs of the admissibility for the ordinary cut rule as well as the elimination of a second cut rule, which manipulates enhanced hypotheses. Furthermore, we make available a formal verification of the equivalence of this proposal with the previously defined axiomatic and dual-context natural deduction systems for <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129522000378_inline5.png\"\/><jats:tex-math>\n$\\mathsf{CS4}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, using the Coq proof-assistant.<\/jats:p>","DOI":"10.1017\/s0960129522000378","type":"journal-article","created":{"date-parts":[[2022,11,23]],"date-time":"2022-11-23T13:01:43Z","timestamp":1669208503000},"page":"1205-1233","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["A dual-context sequent calculus for the constructive modal logic S4"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0436-5034","authenticated-orcid":false,"given":"Favio Ezequiel","family":"Miranda-Perea","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4956-1162","authenticated-orcid":false,"given":"Lourdes del Carmen","family":"Gonz\u00e1lez Huesca","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8884-618X","authenticated-orcid":false,"given":"Pilar Selene","family":"Linares Ar\u00e9valo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2022,11,23]]},"reference":[{"key":"S0960129522000378_ref32","article-title":"Structural Proof Theory, Cambridge University","author":"Negri","year":"2001","journal-title":"Press."},{"key":"S0960129522000378_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/1069774.1069778"},{"first-page":"292","year":"2001","author":"Alechina","key":"S0960129522000378_ref1"},{"key":"S0960129522000378_ref25","first-page":"11","article-title":"On the meanings of the logical constants and the justifications of the logical laws","volume":"1","author":"Martin-L\u00f6f","year":"1996","journal-title":"Nordic Journal of Philosophical Logic"},{"first-page":"29","year":"2006","author":"Boella","key":"S0960129522000378_ref6"},{"key":"S0960129522000378_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-011-9905-9"},{"key":"S0960129522000378_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00169-7"},{"key":"S0960129522000378_ref4","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005291931660"},{"key":"S0960129522000378_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/BF02121259"},{"key":"S0960129522000378_ref36","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn071"},{"key":"S0960129522000378_ref31","doi-asserted-by":"publisher","DOI":"10.1111\/j.1747-9991.2011.00418.x"},{"key":"S0960129522000378_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"S0960129522000378_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-6600-6_3"},{"key":"S0960129522000378_ref15","doi-asserted-by":"crossref","unstructured":"Gonz\u00e1lez Huesca, L. , Miranda-Perea, F. E. and Linares-Ar\u00e9valo, P. S. (2020). Dual and axiomatic systems for constructive S4, a formally verified equivalence. Electronic Notes in Theoretical Computer Science 348 61\u201383. ISSN 1571-0661. doi:https:\/\/doi.org\/10.1016\/j.entcs.2020.02.005. 14th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2019).","DOI":"10.1016\/j.entcs.2020.02.005"},{"key":"S0960129522000378_ref35","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"S0960129522000378_ref11","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2627"},{"key":"S0960129522000378_ref34","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2832"},{"key":"S0960129522000378_ref38","volume-title":"Trends in Logic","volume":"32","author":"Poggiolesi","year":"2010"},{"key":"S0960129522000378_ref43","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(90)90059-B"},{"key":"S0960129522000378_ref33","first-page":"113","article-title":"Gentzen method in modal calculi","volume":"9","author":"Ohnishi","year":"1957","journal-title":"Osaka Mathematical Journal"},{"key":"S0960129522000378_ref42","article-title":"Elements of Logical Reasoning, Cambridge University","author":"von Plato","year":"2014","journal-title":"Press."},{"first-page":"69","year":"2004","author":"Moody","key":"S0960129522000378_ref28"},{"key":"S0960129522000378_ref5","unstructured":"Bobillo, F. , Cerami, M. , Esteva, F. , Garc\u00eda-Cerda\u00f1a, A. , Pe\u00f1aloza, R. and Straccia, U. (2015). Fuzzy description logics. In: Cintula, P., Ferm\u00fcller, C. and Noguera, C. (eds.) Handbook of Mathematical Fuzzy Logic, Studies in Logic, Mathematical Logic and Foundations, vol. 3, chapter XVI, College Publications."},{"key":"S0960129522000378_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3208-5"},{"volume-title":"Studies in Universal Logic","year":"2021","author":"Indrzejczak","key":"S0960129522000378_ref21"},{"key":"S0960129522000378_ref37","doi-asserted-by":"crossref","unstructured":"Plotkin, G. and Stirling, C. (1986). A framework for intuitionistic modal logics: Extended abstract. In: Proceedings of the 1986 Conference on Theoretical Aspects of Reasoning about Knowledge, TARK\u201986, San Francisco, CA, USA, Morgan Kaufmann Publishers Inc., 399\u2013406. ISBN 0934613049.","DOI":"10.1016\/B978-0-934613-04-0.50032-6"},{"key":"S0960129522000378_ref22","article-title":"Dual-context calculi for modal logic","volume":"16","author":"Kavvos","year":"2020","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129522000378_ref7","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/43.4.274"},{"key":"S0960129522000378_ref39","unstructured":"Simpson, A. K. (1994). The Proof Theory and Semantics of Intuitionistic Modal Logic. Phd thesis, University of Edinburgh."},{"key":"S0960129522000378_ref27","doi-asserted-by":"crossref","unstructured":"Miranda-Perea, F. E. , Gonz\u00e1lez Huesca, L. and Linares-Ar\u00e9valo, P. S. (2020). On interactive proof-search for constructive modal necessity. Electronic Notes in Theoretical Computer Science 354 107\u2013127. ISSN 1571-0661. doi:https:\/\/doi.org\/10.1016\/j.entcs.2020.10.009. Proceedings of the Eleventh and Twelfth Latin American Workshop on Logic\/Languages, Algorithms and New Methods of Reasoning (LANMR).","DOI":"10.1016\/j.entcs.2020.10.009"},{"key":"S0960129522000378_ref40","unstructured":"Sticht, M. (2018). Proof Search in Multi-Agent Dialogues for Modal Logic. Phd thesis, University of Bamberg Press, Universit\u00e4tsbibliothek Bamberg. doctoralthesis."},{"key":"S0960129522000378_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s10986-012-9151-y"},{"key":"S0960129522000378_ref19","unstructured":"Heilala, S. and Pientka, B. (2007b). Bidirectional decision procedures for the intuitionistic propositional modal logic IS4. Technical Report SOCS-TR-2007.2, School of Computer Science, McGill University, Montreal, Canada."},{"key":"S0960129522000378_ref3","unstructured":"Barber, A. and Plotkin, G. (1997). Dual Intuitionistic Linear Logic. Technical Report LFCS-96-347, University of Edinburgh."},{"year":"2011","author":"Grossi","key":"S0960129522000378_ref16"},{"key":"S0960129522000378_ref14","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2019.1647653"},{"key":"S0960129522000378_ref9","doi-asserted-by":"publisher","DOI":"10.2307\/2266613"},{"key":"S0960129522000378_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_9"},{"key":"S0960129522000378_ref8","volume-title":"A Theory of Formal Deducibility","volume":"6","author":"Curry","year":"1950"},{"key":"S0960129522000378_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"S0960129522000378_ref29","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.7"},{"volume-title":"Studies in Proof Theory","year":"1984","author":"Martin-L\u00f6f","key":"S0960129522000378_ref26"},{"key":"S0960129522000378_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-8785-0"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000378","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,29]],"date-time":"2023-03-29T02:33:37Z","timestamp":1680057217000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000378\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10]]},"references-count":43,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["S0960129522000378"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000378","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2022,10]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}