{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T21:52:39Z","timestamp":1769550759488,"version":"3.49.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030860585","type":"print"},{"value":"9783030860592","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-86059-2_26","type":"book-chapter","created":{"date-parts":[[2021,8,31]],"date-time":"2021-08-31T17:48:17Z","timestamp":1630432097000},"page":"446-465","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["The Do\u0161en Square Under Construction: A\u00a0Tale of Four Modalities"],"prefix":"10.1007","author":[{"given":"Michael","family":"Mendler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Scheele","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luke","family":"Burke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,8,30]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Acclavio, M., Catta, D., Stra\u00dfburger, L.: Towards a denotational semantics for proofs in constructive modal logic. arXiv preprint arXiv:2104.09115 (2021)","DOI":"10.1007\/978-3-030-86059-2_25"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Arisaka, R., Das, A., Stra\u00dfburger, L.: On nested sequents for constructive modal logics. Logical Methods in Computer Science 11 (2015)","DOI":"10.2168\/LMCS-11(3:7)2015"},{"key":"26_CR3","unstructured":"Bellin, G., de Paiva, V., Ritter, E.: Extended Curry-Howard correspondence for a basic constructive modal logic. In: Methods for Modalities II (2001)"},{"issue":"2","key":"26_CR4","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1017\/S0956796898002998","volume":"8","author":"N Benton","year":"1998","unstructured":"Benton, N., Bierman, G., de Paiva, V.: Computational types from a logical perspective. J. Funct. Program. 8(2), 177\u2013193 (1998)","journal-title":"J. Funct. Program."},{"key":"26_CR5","doi-asserted-by":"publisher","first-page":"763","DOI":"10.2977\/prims\/1195169271","volume":"27","author":"S Blamey","year":"1991","unstructured":"Blamey, S., Humberstone, L.: A perspective on modal sequent logic. Publ. Res. Inst. Math. Sci. 27, 763\u2013782 (1991)","journal-title":"Publ. Res. Inst. Math. Sci."},{"issue":"3","key":"26_CR6","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/BF02429840","volume":"43","author":"M Bo\u017ei\u0107","year":"1984","unstructured":"Bo\u017ei\u0107, M., Do\u0161en, K.: Models for normal intuitionistic modal logics. Studia Logica 43(3), 217\u2013245 (1984)","journal-title":"Studia Logica"},{"key":"26_CR7","unstructured":"Cabalar, P., Odintsov, S.P., Pearce, D.: Logical foundations of well-founded semantics. In: P.D. et al. (ed.) Proceedings of International Conference on Knowledge Representation and Reasoning (2006)"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Dalmonte, T., Grellois, C., Olivetti, N.: Intuitionistic non-normal modal logics: a general framework. J. Philos. Logic 49, 833\u2013882 (2020)","DOI":"10.1007\/s10992-019-09539-3"},{"key":"26_CR9","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-94-015-9309-0_4","volume-title":"What is Negation?","author":"K Do\u0161en","year":"1999","unstructured":"Do\u0161en, K.: Negation in the light of modal logic. In: Gabbay, D.M., Wansing, H. (eds.) What is Negation?, pp. 77\u201386. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-94-015-9309-0_4"},{"issue":"49","key":"26_CR10","first-page":"3","volume":"35","author":"K Do\u0161en","year":"1984","unstructured":"Do\u0161en, K.: Negative modal operators in intuitionistic logic. Publications de L\u2019Institut Math\u00e9matique 35(49), 3\u201314 (1984)","journal-title":"Publications de L\u2019Institut Math\u00e9matique"},{"issue":"1986","key":"26_CR11","first-page":"15","volume":"20","author":"K Do\u0161en","year":"1986","unstructured":"Do\u0161en, K.: Negation as a modal operator. Rep. Math. Logic 20(1986), 15\u201327 (1986)","journal-title":"Rep. Math. Logic"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Dragalin, A.G.: Mathematical Intuitionism: Introduction to Proof Theory. American Mathematical Society (1988)","DOI":"10.1090\/mmono\/067"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Drobyshevich, S.: Double negation operator in logic $${N}^\\star $$. J. Math. Sci. 205(3) (2015)","DOI":"10.1007\/s10958-015-2254-3"},{"key":"26_CR14","unstructured":"Drobyshevich, S.A., Odintsov, S.P.: Finite model property for negative modalities. Sibirskie Elektronnye Matematicheskie Izvestiia 10 (2013)"},{"key":"26_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10469-013-9235-8","volume":"52","author":"SA Drobyshevich","year":"2013","unstructured":"Drobyshevich, S.A.: Composition of an intuitionistic negation and negative modalities as a necessity operator. Algebra Logic 52, 1\u201319 (2013). https:\/\/doi.org\/10.1007\/s10469-013-9235-8","journal-title":"Algebra Logic"},{"issue":"1","key":"26_CR16","first-page":"79","volume":"24","author":"S Drobyshevich","year":"2015","unstructured":"Drobyshevich, S.: On classical behavior of intuitionistic modalities. Logic Log. Philos. 24(1), 79\u2013104 (2015)","journal-title":"Logic Log. Philos."},{"key":"26_CR17","doi-asserted-by":"publisher","first-page":"331","DOI":"10.2307\/2214128","volume":"7","author":"JM Dunn","year":"1993","unstructured":"Dunn, J.M.: Star and perp: two treatments of negation. Philos. Perspect. 7, 331\u2013357 (1993)","journal-title":"Philos. Perspect."},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Dunn, J.M.: Negation, a notion in focus, vol. 7, chap. Generalized Ortho Negation, pp. 3\u201326. Walter de Gruyter Berlin (1996)","DOI":"10.1515\/9783110876802.3"},{"issue":"2\u20133","key":"26_CR19","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s11225-005-8470-y","volume":"80","author":"JM Dunn","year":"2005","unstructured":"Dunn, J.M., Zhou, C.: Negation in the context of gaggle theory. Studia Logica 80(2\u20133), 235\u2013264 (2005). https:\/\/doi.org\/10.1007\/s11225-005-8470-y","journal-title":"Studia Logica"},{"issue":"1","key":"26_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M Fairtlough","year":"1997","unstructured":"Fairtlough, M., Mendler, M.: Propositional lax logic. Inf. Comput. 137(1), 1\u201333 (1997)","journal-title":"Inf. Comput."},{"key":"26_CR21","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1093\/oso\/9780198537458.003.0006","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"M Fitting","year":"1993","unstructured":"Fitting, M.: Basic modal logic. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 1, pp. 368\u2013448. Oxford University Press, New York (1993)"},{"issue":"3","key":"26_CR22","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/s10817-009-9151-8","volume":"44","author":"M Mendler","year":"2010","unstructured":"Mendler, M., Scheele, S.: Towards constructive DL for abstraction and refinement. J. Autom. Reason. 44(3), 207\u2013243 (2010). https:\/\/doi.org\/10.1007\/s10817-009-9151-8","journal-title":"J. Autom. Reason."},{"issue":"12","key":"26_CR23","doi-asserted-by":"publisher","first-page":"1465","DOI":"10.1016\/j.ic.2011.10.003","volume":"209","author":"M Mendler","year":"2011","unstructured":"Mendler, M., Scheele, S.: Cut-free Gentzen calculus for multimodal CK. Inf. Comput. 209(12), 1465\u20131490 (2011)","journal-title":"Inf. Comput."},{"key":"26_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/FI-2014-984","volume":"130","author":"M Mendler","year":"2014","unstructured":"Mendler, M., Scheele, S.: On the computational interpretation of CK$$_n$$. Fundamenta Informaticae 130, 1\u201339 (2014)","journal-title":"Fundamenta Informaticae"},{"key":"26_CR25","unstructured":"Mendler, M., de Paiva, V.: Constructive CK for contexts. In: Proceedings of the First Workshop on Context Representation and Reasoning, CONTEXT 2005 (2005)"},{"issue":"1","key":"26_CR26","doi-asserted-by":"publisher","first-page":"16","DOI":"10.2307\/2268973","volume":"14","author":"D Nelson","year":"1949","unstructured":"Nelson, D.: Constructible falsity. J. Symb. Logic 14(1), 16\u201326 (1949)","journal-title":"J. Symb. Logic"},{"key":"26_CR27","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10992-020-09558-5","volume":"50","author":"S Odintsov","year":"2020","unstructured":"Odintsov, S., Wansing, H.: Routley star and hyperintensionality. J. Philos. Logic 50, 33\u201356 (2020)","journal-title":"J. Philos. Logic"},{"key":"26_CR28","unstructured":"Odintsov, S.P.: Combining intuitionistic connectives and Routley negation. In: Siberian Electronic Mathematical Reports (2005)"},{"key":"26_CR29","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Stirling, C.: A framework for intuitionistic modal logics. In: Halpern, J. (ed.) Theoretical Aspects of Reasoning About Knowledge, pp. 399\u2013406. Monterey (1986)","DOI":"10.1016\/B978-0-934613-04-0.50032-6"},{"key":"26_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-9670-8","volume-title":"Gentzen Calculi for Modal and Propositional Logic","author":"F Poggiolesi","year":"2011","unstructured":"Poggiolesi, F.: Gentzen Calculi for Modal and Propositional Logic. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-90-481-9670-8"},{"key":"26_CR31","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983382","volume-title":"First Steps in Modal Logic","author":"S Popkorn","year":"1994","unstructured":"Popkorn, S.: First Steps in Modal Logic. Cambridge University Press, Cambridge (1994)"},{"key":"26_CR32","doi-asserted-by":"publisher","first-page":"381","DOI":"10.2977\/prims\/1195189814","volume":"13","author":"M Sato","year":"1977","unstructured":"Sato, M.: A study of Kripke-type models for some modal logics by Gentzen\u2019s sequential method. Publ. Res. Inst. Math. Sci. 13, 381\u2013468 (1977)","journal-title":"Publ. Res. Inst. Math. Sci."},{"key":"26_CR33","doi-asserted-by":"crossref","unstructured":"Scheele, S.: Model and Proof Theory of Constructive ALC, Constructive Description Logics. Ph.D. thesis, University of Bamberg (2015)","DOI":"10.20378\/irb-21626"},{"key":"26_CR34","unstructured":"Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh, Scottland (1994)"},{"key":"26_CR35","unstructured":"Sotirov, V.H.: Modal theories with intuitionistic logic. In: Proceedings of the Conference on Mathematical Logic, Sophia, pp. 139\u2013171 (1980)"},{"key":"26_CR36","doi-asserted-by":"crossref","unstructured":"Speranski, S.O.: Negation as a modality in a quantified setting. J, Logic Comput. (2021)","DOI":"10.1093\/logcom\/exab025"},{"key":"26_CR37","series-title":"Outstanding Contributions to Logic","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-319-29300-4_10","volume-title":"J. Michael Dunn on Information Based Logics","author":"H Wansing","year":"2016","unstructured":"Wansing, H.: On split negation, strong negation, information, falsification, and verification. In: Bimb\u00f3, K. (ed.) J. Michael Dunn on Information Based Logics. OCL, vol. 8, pp. 161\u2013189. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29300-4_10"},{"key":"26_CR38","unstructured":"Westerst\u00e5hl, D.: On the Aristotelian square of opposition. Kapten Mnemos Kolumbarium, en festskrift med anledning av Helge Malmgrens (2005)"},{"key":"26_CR39","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 logic I. Ann. Pure Appl. Logic 50, 271\u2013301 (1990)","journal-title":"Ann. Pure Appl. Logic"},{"key":"26_CR40","unstructured":"Wolter, F., Zakharyaschev, M.: Intuitionistic modal logics as fragments of classical bimodal logics. Logic at work, pp. 168\u2013186 (1997)"},{"issue":"2","key":"26_CR41","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/BF02672476","volume":"36","author":"F Wolter","year":"1997","unstructured":"Wolter, F., Zakharyaschev, M.: The relation between intuitionistic and classical modal logics. Algebra Logic 36(2), 73\u201392 (1997)","journal-title":"Algebra Logic"},{"key":"26_CR42","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-94-017-2109-7_17","volume-title":"Logic and Foundations of Mathematics","author":"F Wolter","year":"1999","unstructured":"Wolter, F., Zakharyaschev, M.: Intuitionistic modal logic. In: Cantini, A., Casari, E., Minari, P. (eds.) Logic and Foundations of Mathematics, pp. 227\u2013238. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-94-017-2109-7_17"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-86059-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T13:55:53Z","timestamp":1725717353000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-86059-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030860585","9783030860592"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-86059-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"30 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Birmingham","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2021","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":"tableaux2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tableaux2021.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}