{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:24Z","timestamp":1759017924219,"version":"3.44.0"},"publisher-location":"Cham","reference-count":30,"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":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper considers the bi-modal logic with both <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\Box $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mo>\u25a1<\/mml:mo>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\u00a0and <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\Diamond $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mo>\u25ca<\/mml:mo>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> arising from Kripke models with crisp accessibility\u00a0whose propositions are valued over the standard G\u00f6del algebra [0,\u00a01]. Since this logic lacks the finite model property, we\u00a0study the logic <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textbf{GW}^\\textrm{c}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msup>\n                    <mml:mi>GW<\/mml:mi>\n                    <mml:mtext>c<\/mml:mtext>\n                  <\/mml:msup>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> relying on <jats:italic>witnessed<\/jats:italic> Kripke models where, for each modal formula, there is an assignment where the formula without the modality takes the same value as the modal one.\u00a0We provide a cut-free sequent calculus and we exploit it to prove\u00a0that <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textbf{GW}^\\textrm{c}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msup>\n                    <mml:mi>GW<\/mml:mi>\n                    <mml:mtext>c<\/mml:mtext>\n                  <\/mml:msup>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> is decidable and meets the finite model property. Finally, we explore a connection between the witnessed models\u00a0and the well-known bi-relational Kripke semantics.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_8","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:12Z","timestamp":1758969912000},"page":"141-160","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A G\u00f6del Modal Logic over\u00a0Witnessed Crisp Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7904-1125","authenticated-orcid":false,"given":"Mauro","family":"Ferrari","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2152-7488","authenticated-orcid":false,"given":"Camillo","family":"Fiorentini","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7551-2877","authenticated-orcid":false,"given":"Ricardo Oscar","family":"Rodriguez","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Baaz, M., Ferm\u00fcller, C.G.: Analytic calculi for projective logics. In: Murray, N.V. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. LNCS, vol. 1617, pp. 36\u201350. Springer, Berlin, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48754-9_8","DOI":"10.1007\/3-540-48754-9_8"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Balbiani, P., Gao, H., Gencer, \u00c7., Olivetti, N.: Local intuitionistic modal logics and their calculi. In: Benzm\u00fcller, C., Heule, M.J., Schmidt, R.A. (eds.) Automated Reasoning. IJCAR 2024. LNCS, vol. 14740, pp. 78\u201396. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63501-4_5","DOI":"10.1007\/978-3-031-63501-4_5"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Beckmann, A., Preining, N.: Linear Kripke frames and G\u00f6del logics. J. Symb. Log. 72(1), 26\u201344 (2007). https:\/\/doi.org\/10.2178\/JSL\/1174668382","DOI":"10.2178\/JSL\/1174668382"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"B\u00edlkov\u00e1, M., Frittella, S., Kozhemiachenko, D.: Paraconsistent g\u00f6del modal logic. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning. IJCAR 2022. LNCS, vol. 13385, pp. 429\u2013448. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_26","DOI":"10.1007\/978-3-031-10769-6_26"},{"issue":"5","key":"8_CR6","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1093\/LOGCOM\/EXP062","volume":"21","author":"F Bou","year":"2011","unstructured":"Bou, F., Esteva, F., Godo, L., Rodr\u00edguez, R.O.: On the minimum many-valued modal logic over a finite residuated lattice. J. Log. Comput. 21(5), 739\u2013790 (2011). https:\/\/doi.org\/10.1093\/LOGCOM\/EXP062","journal-title":"J. Log. Comput."},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Burns, S., Zach, R.: Cut-free completeness for modular hypersequent calculi for modal logics K, T, and D. Rev. Symb. Log. 14(4), 910\u2013929 (2020). https:\/\/doi.org\/10.1017\/s1755020320000180","DOI":"10.1017\/s1755020320000180"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/J.JCSS.2017.03.012","volume":"88","author":"X Caicedo","year":"2017","unstructured":"Caicedo, X., Metcalfe, G., Rodr\u00edguez, R.O., Rogger, J.: Decidability of order-based modal logics. J. Comput. Syst. Sci. 88, 53\u201374 (2017). https:\/\/doi.org\/10.1016\/J.JCSS.2017.03.012","journal-title":"J. Comput. Syst. Sci."},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Caicedo, X., Rodr\u00edguez, R.O.: Standard G\u00f6del modal logics. Stud. Log. 94(2), 189\u2013214 (2010). https:\/\/doi.org\/10.1007\/S11225-010-9230-1","DOI":"10.1007\/S11225-010-9230-1"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Caicedo, X., Rodr\u00edguez, R.O.: Bi-modal G\u00f6del logic over [0,1]-valued Kripke frames. J. Log. Comput. 25(1), 37\u201355 (2015). https:\/\/doi.org\/10.1093\/LOGCOM\/EXS036","DOI":"10.1093\/LOGCOM\/EXS036"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s10817-012-9252-7","volume":"51","author":"M Ferrari","year":"2013","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models. J. Autom. Reason. 51(2), 129\u2013149 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9252-7","journal-title":"J. Autom. Reason."},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Ferrari, M., Fiorentini, C., Fiorino, G.: JTabWb: a java framework for implementing terminating sequent and tableau calculi. Fund. Inform. 150(1), 119\u2013142 (2017). https:\/\/doi.org\/10.3233\/FI-2017-1462","DOI":"10.3233\/FI-2017-1462"},{"key":"8_CR13","unstructured":"Ferrari, M., Fiorentini, C., Rodriguez, R.O.: Implementation of a refutation calculus for the G\u00f6del modal logic over witnessed crisp models (GWC). https:\/\/github.com\/ferram\/jtabwb_provers\/tree\/master\/gwc_ref"},{"issue":"3","key":"8_CR14","doi-asserted-by":"publisher","first-page":"771","DOI":"10.1093\/logcom\/exab014","volume":"31","author":"C Fiorentini","year":"2021","unstructured":"Fiorentini, C., Ferrari, M.: A forward internal calculus for model generation in s4. J. Log. Comput. 31(3), 771\u2013796 (2021). https:\/\/doi.org\/10.1093\/logcom\/exab014","journal-title":"J. Log. Comput."},{"issue":"3\u20134","key":"8_CR15","first-page":"235","volume":"15","author":"MC Fitting","year":"1991","unstructured":"Fitting, M.C.: Many-valued modal logics. Fund. Inform. 15(3\u20134), 235\u2013254 (1991)","journal-title":"Fund. Inform."},{"issue":"1\u20132","key":"8_CR16","first-page":"55","volume":"17","author":"MC Fitting","year":"1992","unstructured":"Fitting, M.C.: Many-valued modal logics ii. Fund. Inform. 17(1\u20132), 55\u201373 (1992)","journal-title":"Fund. Inform."},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Flaminio, T., Godo, L., Mench\u00f3n, P., Rodr\u00edguez, R.O.: Algebras and relational frames for G\u00f6del modal logic and some of its extensions. In: Coniglio, M., Kubyshkina, E., Zaitsev, D. (eds.) Many-valued Semantics and Modal Logics: Essays in Honour of Yuriy Vasilievich Ivlev, pp. 179\u2013216. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-56595-3_7","DOI":"10.1007\/978-3-031-56595-3_7"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Galmiche, D., Salhi, Y.: A family of G\u00f6del hybrid logics. J. Appl. Log. 8(4), 371\u2013385 (2010). https:\/\/doi.org\/10.1016\/J.JAL.2010.08.008","DOI":"10.1016\/J.JAL.2010.08.008"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Hansoul, G., Teheux, B.: Extending \u0141ukasiewicz logics with a modality: algebraic approach to relational semantics. Stud. Log. 101(3), 505\u2013545 (2013). https:\/\/doi.org\/10.1007\/S11225-012-9396-9","DOI":"10.1007\/S11225-012-9396-9"},{"issue":"4","key":"8_CR20","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1023\/A:1019915908844","volume":"11","author":"N Kamide","year":"2002","unstructured":"Kamide, N.: Kripke semantics for modal substructural logics. J. Log. Lang. Inform. 11(4), 453\u2013470 (2002). https:\/\/doi.org\/10.1023\/A:1019915908844","journal-title":"J. Log. Lang. Inform."},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Metcalfe, G., Olivetti, N.: Proof systems for a G\u00f6del modal logic. In: Giese, M., Waaler, A. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2009. LNCS, vol.\u00a05607, pp. 265\u2013279. Springer, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02716-1_20","DOI":"10.1007\/978-3-642-02716-1_20"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Metcalfe, G., Olivetti, N.: Towards a proof theory of G\u00f6del modal logics. Log. Methods Comput. Sci. 7(2) (2011). https:\/\/doi.org\/10.2168\/LMCS-7(2:10)2011","DOI":"10.2168\/LMCS-7(2:10)2011"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Ono, H.: Semantics for substructural logics. In: Schroeder-Heister, P., Do\u0161en, K. (eds.) Substructural Logics, pp. 259\u2013291. Oxford University Press (1993). https:\/\/doi.org\/10.1007\/978-94-017-3598-8_8","DOI":"10.1007\/978-94-017-3598-8_8"},{"issue":"2","key":"8_CR24","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1017\/S1755020308080179","volume":"1","author":"G Priest","year":"2008","unstructured":"Priest, G.: Many-valued modal logics: a simple approach. Rev. Symb. Log. 1(2), 190\u2013203 (2008). https:\/\/doi.org\/10.1017\/S1755020308080179","journal-title":"Rev. Symb. Log."},{"key":"8_CR25","unstructured":"Prud\u2019homme, C., Godet, A., Fages, J.G.: Choco-solver: an open-source java library for constraint programming. https:\/\/github.com\/chocoteam\/choco-solver"},{"issue":"141\/142","key":"8_CR26","first-page":"303","volume":"36","author":"G Restall","year":"1993","unstructured":"Restall, G.: Modalities in substructural logics. Logique et Anal. (N.S.) 36(141\/142), 303\u2013321 (1993)","journal-title":"Logique et Anal. (N.S.)"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, R.O., Vidal, A.: Axiomatization of crisp G\u00f6del modal logic. Stud. Log. 109(2), 367\u2013395 (2021). https:\/\/doi.org\/10.1007\/S11225-020-09910-5","DOI":"10.1007\/S11225-020-09910-5"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Troelstra, A., Schwichtenberg, H.: Basic proof theory, 2nd ed. Cambridge Tracts in Theoretical Computer Science, vol.\u00a043. Cambridge University Press, Cambridge (2000). https:\/\/doi.org\/10.1017\/CBO9781139168717","DOI":"10.1017\/CBO9781139168717"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Vidal, A.: Mniblos: a SMT-based solver for continuous t-norm based logics and some of their modal expansions. Inf. Sci. 372, 709\u2013730 (2016). https:\/\/doi.org\/10.1016\/J.INS.2016.08.072","DOI":"10.1016\/J.INS.2016.08.072"},{"issue":"1","key":"8_CR30","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1093\/LOGCOM\/EXV046","volume":"27","author":"A Vidal","year":"2017","unstructured":"Vidal, A., Esteva, F., Godo, L.: On modal extensions of product fuzzy logic. J. Log. Comput. 27(1), 299\u2013336 (2017). https:\/\/doi.org\/10.1093\/LOGCOM\/EXV046","journal-title":"J. Log. Comput."}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:13Z","timestamp":1758969913000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_8","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"}}]}}