{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T20:44:31Z","timestamp":1783111471766,"version":"3.54.6"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031626869","type":"print"},{"value":"9783031626876","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-62687-6_4","type":"book-chapter","created":{"date-parts":[[2024,6,7]],"date-time":"2024-06-07T15:01:50Z","timestamp":1717772510000},"page":"47-63","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Simple Loopcheck for\u00a0Intuitionistic K"],"prefix":"10.1007","author":[{"given":"Marianna","family":"Girlando","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roman","family":"Kuznets","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sonia","family":"Marin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marianela","family":"Morales","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lutz","family":"Stra\u00dfburger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,6,8]]},"reference":[{"key":"4_CR1","unstructured":"Bellin, G., de\u00a0Paiva, V., Ritter, E.: Extended Curry\u2013Howard correspondence for a basic constructive modal logic. In: Areces, C., de\u00a0Rijke, M. (eds.) Workshop Proceedings of Methods for Modalities, vol. 2 (2001)"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Fischer Servi, G.: Semantics for a class of intuitionistic modal calculi. In: Dalla\u00a0Chiara, M.L. (ed.) Italian Studies in the Philosophy of Science, Boston Studies in the Philosophy of Science, vol.\u00a047, pp. 59\u201372. D.\u00a0Reidel Publishing Company (1980). https:\/\/doi.org\/10.1007\/978-94-009-8937-5_5","DOI":"10.1007\/978-94-009-8937-5_5"},{"issue":"3","key":"4_CR3","first-page":"179","volume":"42","author":"G Fischer Servi","year":"1984","unstructured":"Fischer Servi, G.: Axiomatizations for some intuitionistic modal logics. Rendiconti del Seminario Matematico, Universit\u00e0 e Politecnico di Torino 42(3), 179\u2013194 (1984)","journal-title":"Rendiconti del Seminario Matematico, Universit\u00e0 e Politecnico di Torino"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Girlando, M., Kuznets, R., Marin, S., Morales, M., Stra\u00dfburger, L.: Intuitionistic\u00a0S4 is decidable. In: 2023\u00a038th\u00a0Annual ACM\/IEEE\u00a0Symposium on Logic in Computer Science\u00a0(LICS), 26\u201329\u00a0June\u00a02023, Boston, USA. IEEE (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175684","DOI":"10.1109\/LICS56636.2023.10175684"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-030-51054-1_25","volume-title":"Automated Reasoning","author":"M Girlando","year":"2020","unstructured":"Girlando, M., Stra\u00dfburger, L.: MOIN: a nested sequent theorem prover for intuitionistic modal logics (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 398\u2013407. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_25"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Kavvos, G.A.: The many worlds of modal $$\\lambda $$-calculi: I. Curry\u2013Howard for necessity, possibility and time. Eprint 1605.08106, arXiv (2016). https:\/\/doi.org\/10.48550\/arXiv.1605.08106","DOI":"10.48550\/arXiv.1605.08106"},{"issue":"3\u20134","key":"4_CR7","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/s00153-018-0636-1","volume":"58","author":"R Kuznets","year":"2019","unstructured":"Kuznets, R., Stra\u00dfburger, L.: Maehara-style modal nested calculi. Arch. Math. Logic 58(3\u20134), 359\u2013385 (2019). https:\/\/doi.org\/10.1007\/s00153-018-0636-1","journal-title":"Arch. Math. Logic"},{"issue":"14","key":"4_CR8","doi-asserted-by":"publisher","first-page":"2677","DOI":"10.1007\/s11229-012-0061-7","volume":"190","author":"P Maffezioli","year":"2013","unstructured":"Maffezioli, P., Naibo, A., Negri, S.: The Church-Fitch knowability paradox in the light of structural proof theory. Synthese 190(14), 2677\u20132716 (2013). https:\/\/doi.org\/10.1007\/s11229-012-0061-7","journal-title":"Synthese"},{"issue":"3","key":"4_CR9","doi-asserted-by":"publisher","first-page":"998","DOI":"10.1093\/logcom\/exab020","volume":"31","author":"S Marin","year":"2021","unstructured":"Marin, S., Morales, M., Stra\u00dfburger, L.: A fully labelled proof system for intuitionistic modal logics. J. Log. Comput. 31(3), 998\u20131022 (2021). https:\/\/doi.org\/10.1093\/logcom\/exab020","journal-title":"J. Log. Comput."},{"key":"4_CR10","unstructured":"Morales, M.: Unusual proof systems for modal logics with applications to decision problems. Ph.D. thesis, Polytechnic Institute of Paris, Palaiseau, France (2023). https:\/\/theses.hal.science\/tel-04546959. Prepared at \u00c9cole polytechnique"},{"issue":"1","key":"4_CR11","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s11787-014-0097-1","volume":"8","author":"S Negri","year":"2014","unstructured":"Negri, S.: Proofs and countermodels in non-classical logics. Log. Univers. 8(1), 25\u201360 (2014). https:\/\/doi.org\/10.1007\/s11787-014-0097-1","journal-title":"Log. Univers."},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Stirling, C.: A framework for intuitionistic modal logics. In: Halpern, J.Y. (ed.) Theoretical Aspects of Reasoning About Knowledge: Proceedings of the 1986 Conference, pp. 399\u2013406. Morgan Kaufmann (1986). https:\/\/dl.acm.org\/doi\/10.5555\/1029786.1029823","DOI":"10.1016\/B978-0-934613-04-0.50032-6"},{"key":"4_CR13","unstructured":"Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh, Edinburgh, Scotland, UK (1994). http:\/\/hdl.handle.net\/1842\/407"},{"issue":"3","key":"4_CR14","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/0168-0072(90)90059-B","volume":"50","author":"D Wijesekera","year":"1990","unstructured":"Wijesekera, D.: Constructive modal logics I. Ann. Pure Appl. Logic 50(3), 271\u2013301 (1990). https:\/\/doi.org\/10.1016\/0168-0072(90)90059-B","journal-title":"Ann. Pure Appl. Logic"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-62687-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,7]],"date-time":"2024-06-07T15:02:18Z","timestamp":1717772538000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-62687-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031626869","9783031626876"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-62687-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"8 June 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WoLLIC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Logic, Language, Information, and Computation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bern","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Switzerland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wollic2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/wollic2024.inf.unibe.ch\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}