{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T10:13:42Z","timestamp":1775470422290,"version":"3.50.1"},"publisher-location":"Cham","reference-count":26,"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>We consider intuitionistic multimodal logics with modalities satisfying axiom K and the axiom of Necessity, as well as collections of axioms for transforming, removing and splitting modalities, specified by a relation between modalities and sequences of modalities. These axioms can be used for systems of knowledge and belief, describing multiple environments of truth and their awareness of each other. We extend Gentzen\u2019s decidable cut-free calculus to accommodate such multimodal systems, using a modal shift operation on contexts to extend the cut elimination proof in a novel way. We then adapt the inverse method to formulate a correct and complete forward proof search for these logics, which can be interpreted in a Fitch-style manner. Proof derivation is streamlined by implementing most derivations using the cut rule. The resulting proof search allows for making multiple queries, building a database of assumptions and their consequences which can be fine-tuned and updated to fit an application.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_18","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:14Z","timestamp":1758969914000},"page":"335-353","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Forward Proof Search for\u00a0Intuitionistic Multimodal K Logics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6650-3493","authenticated-orcid":false,"given":"Niels","family":"Voorneveld","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1017\/S0960129519000197","volume":"30","author":"L Birkedal","year":"2018","unstructured":"Birkedal, L., Clouston, R., Mannaa, B., M\u00f8gelberg, R.E., Pitts, A.M., Spitters, B.: Modal dependent type theory and dependent right adjoints. Math. Struct. Comput. Sci. 30, 118\u2013138 (2018). https:\/\/doi.org\/10.1017\/S0960129519000197","journal-title":"Math. Struct. Comput. Sci."},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11532231_6","volume-title":"Automated Deduction \u2013 CADE-20","author":"K Chaudhuri","year":"2005","unstructured":"Chaudhuri, K., Pfenning, F.: A focusing inverse method theorem prover for first-order linear logic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 69\u201383. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_6"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11814771_9","volume-title":"Automated Reasoning","author":"K Chaudhuri","year":"2006","unstructured":"Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 97\u2013111. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_9"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-319-89366-2_14","volume-title":"Foundations of Software Science and Computation Structures","author":"R Clouston","year":"2018","unstructured":"Clouston, R.: Fitch-style modal lambda calculi. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 258\u2013275. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_14"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Degtyarev, A., Robinson, J., Voronkov, A.: The inverse method. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 179\u2013272. North-Holland, Amsterdam (2001). https:\/\/doi.org\/10.1016\/b978-044450813-3\/50006-0","DOI":"10.1016\/b978-044450813-3\/50006-0"},{"key":"18_CR6","unstructured":"Fitch, F.B.: Symbolic Logic: An Introduction. Roland Press Co., New York (1952)"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Garg, D., Genovese, V., Negri, S.: Countermodels from sequent calculi in multi-modal logics. In: Proceedings of 27th Annual IEEE Symposium on Logic in Computer Science (LICS \u201912), pp. 315\u2013324. IEEE, Los Alamitos, CA (2012). https:\/\/doi.org\/10.1109\/lics.2012.42","DOI":"10.1109\/lics.2012.42"},{"issue":"1","key":"18_CR8","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/bf01201353","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische SchlieSSen. I. Math. Z. 39(1), 176\u2013210 (1935). https:\/\/doi.org\/10.1007\/bf01201353","journal-title":"I. Math. Z."},{"key":"18_CR9","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types, Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Girlando, M., Kuznets, R., Marin, S., Morales, M., StraSSburger, L.: Intuitionistic S4 is decidable. In: Proceedings of 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201923), pp. 1\u201313. IEEE, Los Alamitos, CA (2023). https:\/\/doi.org\/10.1109\/lics56636.2023.10175684","DOI":"10.1109\/lics56636.2023.10175684"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-73595-3_9","volume-title":"Automated Deduction \u2013 CADE-21","author":"S Heilala","year":"2007","unstructured":"Heilala, S., Pientka, B.: Bidirectional decision procedures for the intuitionistic propositional modal logic IS4. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 116\u2013131. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_9"},{"key":"18_CR12","unstructured":"Heyting, A.: Intuitionism: An Introduction, Studies in Logic and the Foundations of Mathematics, vol.\u00a017. North-Holland, Amsterdam (1956). https:\/\/www.sciencedirect.com\/bookseries\/studies-in-logic-and-the-foundations-of-mathematics\/vol\/17"},{"issue":"4","key":"18_CR13","doi-asserted-by":"publisher","first-page":"127","DOI":"10.2307\/2269018","volume":"10","author":"O Ketonen","year":"1945","unstructured":"Ketonen, O.: Untersuchungen zum Pr\u00e4dikatenkalkul. J. Symb. Logic 10(4), 127\u2013130 (1945). https:\/\/doi.org\/10.2307\/2269018","journal-title":"J. Symb. Logic"},{"key":"18_CR14","unstructured":"Kleene, S.C.: Introduction to Metamathematics. P. Noordhoff N.V, Groningen (1952)"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Kripke, S.A.: Semantical analysis of intuitionistic logic I. In: Crossley, J., Dummett, M. (eds.) Formal Systems and Recursive Functions, Studies in Logic and the Foundations of Mathematics, vol.\u00a040, pp. 92\u2013130. Elsevier (1965). https:\/\/doi.org\/10.1016\/s0049-237x(08)71685-9","DOI":"10.1016\/s0049-237x(08)71685-9"},{"key":"18_CR16","doi-asserted-by":"publisher","unstructured":"Maslov, S.Y.: Invertible sequential variant of constructive predicate calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic: Part I, Seminars in Mathematics: V. A. Steklov Mathematical Institute, Leningrad, vol.\u00a04, pp. 36\u201342. Consultants Bureau, New York (1969). https:\/\/doi.org\/10.1007\/978-1-4684-8968-2_10","DOI":"10.1007\/978-1-4684-8968-2_10"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-02959-2_19","volume-title":"Automated Deduction \u2013 CADE-22","author":"S McLaughlin","year":"2009","unstructured":"McLaughlin, S., Pfenning, F.: Efficient intuitionistic theorem proving with the polarized inverse method. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 230\u2013244. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_19"},{"key":"18_CR18","unstructured":"McLaughlin, S., Pfenning, F.: The focused constraint inverse method for intuitionistic modal logics (2010). https:\/\/www.cs.cmu.edu\/~fp\/papers\/inviml10.pdf, manuscript"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/3-540-52335-9_55","volume-title":"COLOG-88","author":"G Mints","year":"1990","unstructured":"Mints, G.: Gentzen-type systems and resolution rules part I propositional logic. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 198\u2013231. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52335-9_55"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press, Cambridge (2001).https:\/\/doi.org\/10.1017\/cbo9780511527340","DOI":"10.1017\/cbo9780511527340"},{"key":"18_CR21","unstructured":"Ono, K.: Logische Untersuchungen \u00fcber die Grundlagen der Mathematik. J. Fac. Sci. Imperial Univ. Tokyo, Section I 3(7), 329\u2013389 (1939)"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Pfenning, F.: Structural cut elimination: I. intuitionistic and classical logic. Inf. Comput. 157(1), 84\u2013141 (2000). https:\/\/doi.org\/10.1006\/inco.1999.2832","DOI":"10.1006\/inco.1999.2832"},{"key":"18_CR23","unstructured":"Simpson, A.K.: The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, University of Edinburgh (1994). https:\/\/hdl.handle.net\/1842\/407"},{"key":"18_CR24","unstructured":"Troelstra, A.S., Dalen, D.: Constructivism in Mathematics: An Introduction, Studies in Logic and the Foundations of Mathematics, vol.\u00a0121. North-Holland, Amsterdam (1988). https:\/\/www.sciencedirect.com\/bookseries\/studies-in-logic-and-the-foundations-of-mathematics\/vol\/121\/"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, vol.\u00a043. Cambridge University Press, 2nd edn. (2000). https:\/\/doi.org\/10.1017\/cbo9781139168717","DOI":"10.1017\/cbo9781139168717"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Wolter, F., Zakharyaschev, M.: Intuitionistic modal logic. In: Cantini, A., Casari, E., Minari, P. (eds.) Logic and Foundations of Mathematics, Synthese Library, vol.\u00a0280, pp. 227\u2013238. Kluwer, Dordrecht (1999). https:\/\/doi.org\/10.1007\/978-94-017-2109-7_17","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_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:15Z","timestamp":1758969915000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_18","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"}}]}}