{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:20Z","timestamp":1759017920181,"version":"3.44.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"Abstract<\/jats:title>\n Intuitionistic conditional logic, studied by Weiss, Ciardelli and Liu, and Olkhovikov, aims at providing a constructive analysis of conditional reasoning. In this framework, the would<\/jats:italic> and the might<\/jats:italic> conditional operators are no longer interdefinable. The intuitionistic conditional logics considered in the literature are defined by setting Chellas\u2019 conditional logic \n \n $$\\textsf{CK}$$<\/jats:tex-math>\n \n CK<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, whose semantics is defined using selection functions, within the constructive and intuitionistic framework introduced for intuitionistic modal logics. This operation gives rise to a constructive variant of might-free-\n \n $$\\textsf{CK}$$<\/jats:tex-math>\n \n CK<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, which we call \n\"Image missing\", and an intuitionistic variant of \n \n $$\\textsf{CK}$$<\/jats:tex-math>\n \n CK<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, called \n \n $$\\textsf{IntCK}$$<\/jats:tex-math>\n \n IntCK<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>. Building on the proof systems defined for \n \n $$\\textsf{CK}$$<\/jats:tex-math>\n \n CK<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> and for intuitionistic modal logics, in this paper we introduce a nested calculus for \n \n $$\\textsf{IntCK}$$<\/jats:tex-math>\n \n IntCK<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> and a sequent calculus for \n\"Image missing\". Based on the sequent calculus, we define \n \n $$\\textsf{ConstCK}$$<\/jats:tex-math>\n \n ConstCK<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, a conservative extension of Weiss\u2019 logic \n\"Image missing\"with the might operator. We introduce a class of models and an axiomatisation for \n \n $$\\textsf{ConstCK}$$<\/jats:tex-math>\n \n ConstCK<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, and extend these result to some extensions of \n \n $$\\textsf{ConstCK}$$<\/jats:tex-math>\n \n ConstCK<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_19","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:15Z","timestamp":1758969915000},"page":"354-373","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Proof-Theoretic View of\u00a0Basic Intuitionistic Conditional Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7153-0506","authenticated-orcid":false,"given":"Tiziano","family":"Dalmonte","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9384-1356","authenticated-orcid":false,"given":"Marianna","family":"Girlando","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-44802-0_21","volume-title":"Computer Science Logic","author":"N Alechina","year":"2001","unstructured":"Alechina, N., Mendler, M., de Paiva, V., Ritter, E.: Categorical and kripke semantics for constructive s4 modal logic. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 292\u2013307. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_21"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-642-33353-8_2","volume-title":"Logics in Artificial Intelligence","author":"R Alenda","year":"2012","unstructured":"Alenda, R., Olivetti, N., Pozzato, G.L.: Nested sequent calculi for conditional logics. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS (LNAI), vol. 7519, pp. 14\u201327. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33353-8_2"},{"issue":"1","key":"19_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1093\/logcom\/ext034","volume":"26","author":"R Alenda","year":"2016","unstructured":"Alenda, R., Olivetti, N., Pozzato, G.L.: Nested sequent calculi for normal conditional logics. J. Log. Comput. 26(1), 7\u201350 (2016)","journal-title":"J. Log. Comput."},{"key":"19_CR4","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. Stud. Logica 43, 217\u2013245 (1984)","journal-title":"Stud. Logica"},{"issue":"6","key":"19_CR5","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00153-009-0137-3","volume":"48","author":"K Br\u00fcnnler","year":"2009","unstructured":"Br\u00fcnnler, K.: Deep sequent systems for modal logic. Arch. Math. Logic 48(6), 551\u2013577 (2009). https:\/\/doi.org\/10.1007\/s00153-009-0137-3","journal-title":"Arch. Math. Logic"},{"issue":"1","key":"19_CR6","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1305\/ndjfl\/1093883341","volume":"22","author":"JP Burgess","year":"1981","unstructured":"Burgess, J.P.: Quick completeness proofs for some logics of conditionals. Notre Dame J. Formal Logic 22(1), 76\u201384 (1981)","journal-title":"Notre Dame J. Formal Logic"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Chellas, B.F.: Basic conditional logic. J. Philosophic. Logic 133\u2013153 (1975)","DOI":"10.1007\/BF00693270"},{"issue":"4","key":"19_CR8","doi-asserted-by":"publisher","first-page":"807","DOI":"10.1007\/S10992-019-09538-4","volume":"49","author":"I Ciardelli","year":"2020","unstructured":"Ciardelli, I., Liu, X.: Intuitionistic conditional logics. J. Philos. Log. 49(4), 807\u2013832 (2020). https:\/\/doi.org\/10.1007\/S10992-019-09538-4","journal-title":"J. Philos. Log."},{"key":"19_CR9","unstructured":"Dalmonte, T., Girlando, M.: A proof-theoretic view of basic intuitionistic conditional logic (extended version) (2025). https:\/\/arxiv.org\/abs\/2507.02767"},{"key":"19_CR10","doi-asserted-by":"publisher","unstructured":"Das, A., Marin, S.: On intuitionistic diamonds (and lack thereof). In: Ramanayake, R., Urban, J. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, 18\u201321 September 2023, Proceedings. Lecture Notes in Computer Science, vol. 14278, pp. 283\u2013301. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-43513-3_16","DOI":"10.1007\/978-3-031-43513-3_16"},{"key":"19_CR11","unstructured":"Dufty, B., de Groot, J.: Filling in the semantics for intuitionistic conditional logic. arXiv:2508.11972 (2025)"},{"key":"19_CR12","doi-asserted-by":"publisher","unstructured":"Fischer Servi, G.: Axiomatizations for some intuitionistic modal logics. Rendiconti del Seminario Matematico - PoliTO 42(3), 179\u2013194 (1984). https:\/\/doi.org\/10.1093\/logcom\/exs040","DOI":"10.1093\/logcom\/exs040"},{"key":"19_CR13","doi-asserted-by":"publisher","unstructured":"Genovese, V., Giordano, L., Gliozzi, V., Pozzato, G.L.: Logics in access control: a conditional approach. J. Log. Comput. 24(4), 705\u2013762 (2014). https:\/\/doi.org\/10.1093\/LOGCOM\/EXS040","DOI":"10.1093\/LOGCOM\/EXS040"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Indrzejczak, A.: Sequents and Trees. Birkh\u00e4user Cham (2021)","DOI":"10.52843\/cassyni.8l6pqd"},{"issue":"3","key":"19_CR15","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), 359\u2013385 (2019)","journal-title":"Arch. Math. Logic"},{"key":"19_CR16","unstructured":"Lewis, D.: Counterfactuals. Blackwell (1973)"},{"issue":"3","key":"19_CR17","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)","journal-title":"J. Log. Comput."},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Olkhovikov, G.K.: An intuitionistically complete system of basic intuitionistic conditional logic. J. Philos. Log. 53(5), 1199\u20131240 (2024). https:\/\/doi.org\/10.1007\/S10992-024-09763-6","DOI":"10.1007\/S10992-024-09763-6"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"Pattinson, D., Schr\u00f6der, L.: Generic modal cut elimination applied to conditional logics. Log. Methods Comput. Sci. 7(1) (2011). https:\/\/doi.org\/10.2168\/LMCS-7(1:4)2011","DOI":"10.2168\/LMCS-7(1:4)2011"},{"key":"19_CR20","doi-asserted-by":"publisher","unstructured":"Schr\u00f6der, L., Pattinson, D., Hausmann, D.: Optimal tableaux for conditional logics with cautious monotonicity. In: Coelho, H., Studer, R., Wooldridge, M.J. (eds.) ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, 16\u201320 August 2010, Proceedings. Frontiers in Artificial Intelligence and Applications, vol.\u00a0215, pp. 707\u2013712. IOS Press (2010). https:\/\/doi.org\/10.3233\/978-1-60750-606-5-707","DOI":"10.3233\/978-1-60750-606-5-707"},{"issue":"1","key":"19_CR21","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1111\/j.1755-2567.1968.tb00337.x","volume":"34","author":"K Segerberg","year":"1968","unstructured":"Segerberg, K.: Propositional logics related to heyting\u2019s and johansson\u2019s. Theoria 34(1), 26\u201361 (1968)","journal-title":"Theoria"},{"key":"19_CR22","unstructured":"Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic (1994)"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-37075-5_14","volume-title":"Foundations of Software Science and Computation Structures","author":"L Stra\u00dfburger","year":"2013","unstructured":"Stra\u00dfburger, L.: Cut elimination in nested sequents for intuitionistic modal logics. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 209\u2013224. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37075-5_14"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press (2000)","DOI":"10.1017\/CBO9781139168717"},{"key":"19_CR25","doi-asserted-by":"publisher","unstructured":"Weiss, Y.: Basic intuitionistic conditional logic. J. Philos. Log. 48(3), 447\u2013469 (2019). https:\/\/doi.org\/10.1007\/S10992-018-9471-4","DOI":"10.1007\/S10992-018-9471-4"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Wi\u0119ckowski, B.: On the proof-theoretic structure of counterfactual inference. Bull. Symb. Logic 1\u201351 (2025)","DOI":"10.1017\/bsl.2025.20"},{"issue":"3","key":"19_CR27","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)","journal-title":"Ann. Pure Appl. Logic"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Wolter, F., Zakharyaschev, M.: Intuitionistic modal logic. In: Logic and Foundations of Mathematics: Selected Contributed Papers of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, pp. 227\u2013238. Springer (1995)","DOI":"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-032-06085-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:17Z","timestamp":1758969917000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","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":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}