{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:31:33Z","timestamp":1740123093055,"version":"3.37.3"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T00:00:00Z","timestamp":1657843200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T00:00:00Z","timestamp":1657843200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["639.073.807"],"award-info":[{"award-number":["639.073.807"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2022,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper provides a method to obtain terminating analytic calculi for a large class of intuitionistic modal logics. For a given logic  with a cut-free calculus  that is an extension of  the method produces a terminating analytic calculus that is an extension of  and equivalent to .  was introduced by Roy Dyckhoff in 1992 as a terminating analogue of the calculus  for intuitionistic propositional logic. Thus this paper can be viewed as an extension of Dyckhoff\u2019s work to intuitionistic modal logic.<\/jats:p>","DOI":"10.1007\/s11225-022-10008-3","type":"journal-article","created":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T12:03:58Z","timestamp":1657886638000},"page":"1493-1506","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["The G4i Analogue of a G3i Sequent Calculus"],"prefix":"10.1007","volume":"110","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9975-9604","authenticated-orcid":false,"given":"Rosalie","family":"Iemhoff","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,15]]},"reference":[{"unstructured":"B\u00edlkov\u00e1, M., Interpolation in Modal Logics, PhD thesis, UK Praha, 2006.","key":"10008_CR1"},{"doi-asserted-by":"crossref","unstructured":"Buss, S.R, An Introduction to Proof Theory, in S.R. Buss, ed., Handbook of Proof Theory, vol. 137 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1998, pp. 1\u201378.","key":"10008_CR2","DOI":"10.1016\/S0049-237X(98)80016-5"},{"key":"10008_CR3","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N Dershowitz","year":"1979","unstructured":"Dershowitz, N., and Z.\u00a0Manna, Proving termination with multiset orderings, Communications of the ACM 22:465\u2013476, 1979.","journal-title":"Communications of the ACM"},{"issue":"1","key":"10008_CR4","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00370809","volume":"44","author":"K Do\u0161en","year":"1985","unstructured":"Do\u0161en, K., Models for Stronger Normal Intuitionistic Modal Logics, Studia Logica 44(1):39\u201370, 1985.","journal-title":"Studia Logica"},{"issue":"3","key":"10008_CR5","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, Journal of Symbolic Logic 57(3):795\u2013807, 1992.","journal-title":"Journal of Symbolic Logic"},{"issue":"3","key":"10008_CR6","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/BF02121259","volume":"36","author":"G Fischer-Servi","year":"1977","unstructured":"Fischer-Servi, G., On Modal Logic with an Intuitionistic Base, Studia Logica 36(3):141\u2013149, 1977.","journal-title":"Studia Logica"},{"doi-asserted-by":"crossref","unstructured":"Gabbay, D.M., and L.L.\u00a0Maxsimova, Interpolation and definability, Clarendon Press, 2005.","key":"10008_CR7","DOI":"10.1093\/acprof:oso\/9780198511748.001.0001"},{"issue":"2","key":"10008_CR8","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1215\/00294527-2021-0011","volume":"62","author":"I van der Giessen","year":"2021","unstructured":"van der Giessen, I., and R.\u00a0Iemhoff, Sequent Calculi for Intuitionistic G\u00f6del-L\u00f6b Logic, Notre Dame Journal of Formal Logic 62(2): 221\u2013246, 2021.","journal-title":"Notre Dame Journal of Formal Logic"},{"unstructured":"van der Giessen, I., and R.\u00a0Iemhoff, Proof Theory for Intuitionistic Strong L\u00f6b Logic, Information and Computation, accepted for publication.","key":"10008_CR9"},{"unstructured":"Hudelmaier, J., A Prolog program for intuitionistic propositional logic, SNS-Bericht 88\u201328, T\u00fcbingen, 1988.","key":"10008_CR10"},{"key":"10008_CR11","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF01627506","volume":"31","author":"J Hudelmaier","year":"1992","unstructured":"Hudelmaier, J., Bounds for cut elimination in intuitionistic propositional logic, Archive for Mathematical Logic 31:331\u2013353, 1992.","journal-title":"Archive for Mathematical Logic"},{"key":"10008_CR12","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","volume":"3","author":"J Hudelmaier","year":"1993","unstructured":"Hudelmaier, J., An O(n log n)\u2013space decision procedure for intuitionistic propositional logic, Journal of Logic and Computation 3:63\u201376, 1993.","journal-title":"Journal of Logic and Computation"},{"issue":"7","key":"10008_CR13","doi-asserted-by":"publisher","first-page":"1701","DOI":"10.1093\/logcom\/exy026","volume":"28","author":"R Iemhoff","year":"2018","unstructured":"Iemhoff, R., Terminating Sequent Calculi for Two Intuitionistic Modal Logics, Journal of Logic and Computation 28(7):1701\u20131712, 2018.","journal-title":"Journal of Logic and Computation"},{"doi-asserted-by":"crossref","unstructured":"Iemhoff, R., Uniform interpolation and sequent calculi in modal logic, Archive for Mathematical Logic 58(1-2):155\u2013181, 2019. Online at https:\/\/link.springer.com\/article\/10.1007\/s00153-018-0629-0.","key":"10008_CR14","DOI":"10.1007\/s00153-018-0629-0"},{"issue":"11","key":"10008_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.apal.2019.05.008","volume":"170","author":"R Iemhoff","year":"2019","unstructured":"Iemhoff, R., Uniform interpolation and the existence of sequent calculi, Annals of Pure and Applied Logic 170(11):1\u201337, 2019.","journal-title":"Annals of Pure and Applied Logic"},{"unstructured":"Jalali, R., and A.\u00a0Tabatabai, Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation, 1808.06258, 2018.","key":"10008_CR16"},{"doi-asserted-by":"crossref","unstructured":"Litak, T., Constructive modalities with provability smack, in: G. Bezhanishvili, ed., Leo Esakia on Duality in Modal and Intuitionistic Logics, vol. 4 of Outstanding Contributions to Logic, Springer, 2014, pp. 179\u2013208.","key":"10008_CR17","DOI":"10.1007\/978-94-017-8860-1_8"},{"issue":"1","key":"10008_CR18","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1016\/j.indag.2017.10.003","volume":"29","author":"T Litak","year":"2018","unstructured":"Litak, T., and A.\u00a0Visser, Lewis meets Brouwer: Constructive Strict Implication, Indagationes Mathematic\u00e6 29(1): 36\u201390, 2018.","journal-title":"Indagationes Mathematic\u00e6"},{"issue":"8","key":"10008_CR19","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1111\/j.1747-9991.2011.00418.x","volume":"6","author":"S Negri","year":"2011","unstructured":"Negri, S., Proof Theory for Modal Logic, Philosophy Compass 6(8):523\u2013538, 2011.","journal-title":"Philosophy Compass"},{"doi-asserted-by":"crossref","unstructured":"de Paiva, V., R.\u00a0Gor\u00e9, R., and M.\u00a0Mendler, Modalities in Constructive Logics and Type Theories. Preface to the special issue on Intuitionistic Modal Logic and Application, Journal of Logic and Computation 14(4):439\u2013446, 2004.","key":"10008_CR20","DOI":"10.1093\/logcom\/14.4.439"},{"issue":"1","key":"10008_CR21","doi-asserted-by":"publisher","first-page":"33","DOI":"10.2307\/2275175","volume":"57","author":"A Pitts","year":"1992","unstructured":"Pitts, A., On an interpretation of second order quantification in first order intuitionistic propositional logic, Journal of Symbolic Logic 57(1):33\u201352, 1992.","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"10008_CR22","first-page":"159","volume":"47","author":"V \u0160vejdar","year":"2006","unstructured":"\u0160vejdar, V., On sequent calculi for intuitionistic propositional logic, Commentationes Mathematicae Universitatis Carolinae 47(1):159\u2013173, 2006.","journal-title":"Commentationes Mathematicae Universitatis Carolinae"},{"unstructured":"Troelstra, A.S. and H.\u00a0Schwichtenberg, Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science 43, Cambridge University Press, 1996.","key":"10008_CR23"},{"unstructured":"Troelstra, A.S., Corrections to Basic Proof Theory, 1998: http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.7.888","key":"10008_CR24"},{"key":"10008_CR25","first-page":"689","volume":"85","author":"NN Vorob\u2019ev","year":"1952","unstructured":"Vorob\u2019ev, N.N., The derivability problem in the constructive propositional calculus with strong negation, Doklady Akademii Nauk SSSR 85:689\u2013692, 1952.","journal-title":"Doklady Akademii Nauk SSSR"},{"issue":"94","key":"10008_CR26","first-page":"37","volume":"2","author":"NN Vorob\u2019ev","year":"1970","unstructured":"Vorob\u2019ev, N.N., A new algorithm for derivability in the constructive propositional calculus, AMS Translations Ser.\u00a02 94:37\u201371, 1970.","journal-title":"AMS Translations Ser."},{"doi-asserted-by":"crossref","unstructured":"Wolter, F., and M. Zakharyaschev, Intuitionistic Modal Logic, in A. Cantini, E. Casari, and P. Minari, eds., Logic and Foundations of Mathematics, vol. 280 of Synthese Library, Springer, 1999, pp. 227\u2013238.","key":"10008_CR27","DOI":"10.1007\/978-94-017-2109-7_17"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-10008-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-022-10008-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-10008-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,25]],"date-time":"2022-11-25T21:07:37Z","timestamp":1669410457000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-022-10008-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,15]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["10008"],"URL":"https:\/\/doi.org\/10.1007\/s11225-022-10008-3","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2022,7,15]]},"assertion":[{"value":"26 August 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 May 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 July 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}