{"data":{"id":"10.48550/arxiv.2609.24922","type":"dois","attributes":{"doi":"10.48550/arxiv.2609.24922","prefix":"10.48550","suffix":"arxiv.2609.24922","identifiers":[{"identifier":"2609.24922","identifierType":"arXiv"}],"alternateIdentifiers":[{"alternateIdentifierType":"arXiv","alternateIdentifier":"2609.24922"}],"creators":[{"name":"Girlando, Marianna","nameType":"Personal","givenName":"Marianna","familyName":"Girlando","affiliation":[],"nameIdentifiers":[]},{"name":"Kuznets, Roman","nameType":"Personal","givenName":"Roman","familyName":"Kuznets","affiliation":[],"nameIdentifiers":[]},{"name":"Marin, Sonia","nameType":"Personal","givenName":"Sonia","familyName":"Marin","affiliation":[],"nameIdentifiers":[]},{"name":"Straßburger, Lutz","nameType":"Personal","givenName":"Lutz","familyName":"Straßburger","affiliation":[],"nameIdentifiers":[]}],"titles":[{"title":"A decision procedure for intuitionistic modal logic IS4 (and IK4)"}],"publisher":"arXiv","container":{},"publicationYear":2026,"subjects":[{"lang":"en","subject":"Logic in Computer Science (cs.LO)","subjectScheme":"arXiv"},{"subject":"FOS: Computer and information sciences","subjectScheme":"Fields of Science and Technology (FOS)"}],"contributors":[],"dates":[{"date":"2026-09-21T17:18:22Z","dateType":"Submitted","dateInformation":"v1"},{"date":"2026-09-22T02:17:53Z","dateType":"Updated","dateInformation":"v1"},{"date":"2026-10-08T16:53:45Z","dateType":"Submitted","dateInformation":"v2"},{"date":"2026-10-09T01:28:47Z","dateType":"Updated","dateInformation":"v2"},{"date":"2026-09","dateType":"Available","dateInformation":"v1"}],"language":null,"types":{"ris":"GEN","bibtex":"misc","citeproc":"article","schemaOrg":"CreativeWork","resourceType":"Article","resourceTypeGeneral":"Preprint"},"relatedIdentifiers":[],"relatedItems":[],"sizes":[],"formats":[],"version":"2","rightsList":[{"rights":"Creative Commons Attribution 4.0 International","rightsUri":"https://creativecommons.org/licenses/by/4.0/legalcode","schemeUri":"https://spdx.org/licenses/","rightsIdentifier":"cc-by-4.0","rightsIdentifierScheme":"SPDX"}],"descriptions":[{"description":"In this paper, we show that the two intuitionistic modal logics IS4 and IK4 are decidable. We provide a constructive decision procedure, that, given a formula, produces either a proof showing the formula to be valid or a finite countermodel falsifying the formula, thus also proving the finite model property for both logics. The main ingredient of our strategy is the introduction of (possibly unsound) loop rules, which encode repeating behaviour in proof search. This paper fixes a previous mistake in our LICS'23 contribution.","descriptionType":"Abstract"},{"description":"corrections of minor technical issues in v1","descriptionType":"Other"}],"geoLocations":[],"fundingReferences":[],"xml":"PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0iVVRGLTgiPz4KPHJlc291cmNlIHhtbG5zPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCIgeG1sbnM6eHNpPSJodHRwOi8vd3d3LnczLm9yZy8yMDAxL1hNTFNjaGVtYS1pbnN0YW5jZSIgeHNpOnNjaGVtYUxvY2F0aW9uPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCBodHRwOi8vc2NoZW1hLmRhdGFjaXRlLm9yZy9tZXRhL2tlcm5lbC00LjMvbWV0YWRhdGEueHNkIj4KICA8aWRlbnRpZmllciBpZGVudGlmaWVyVHlwZT0iRE9JIj4xMC40ODU1MC9BUlhJVi4yNjA5LjI0OTIyPC9pZGVudGlmaWVyPgogIDxhbHRlcm5hdGVJZGVudGlmaWVycz4KICAgIDxhbHRlcm5hdGVJZGVudGlmaWVyIGFsdGVybmF0ZUlkZW50aWZpZXJUeXBlPSJhclhpdiI+MjYwOS4yNDkyMjwvYWx0ZXJuYXRlSWRlbnRpZmllcj4KICA8L2FsdGVybmF0ZUlkZW50aWZpZXJzPgogIDxjcmVhdG9ycz4KICAgIDxjcmVhdG9yPgogICAgICA8Y3JlYXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5HaXJsYW5kbywgTWFyaWFubmE8L2NyZWF0b3JOYW1lPgogICAgICA8Z2l2ZW5OYW1lPk1hcmlhbm5hPC9naXZlbk5hbWU+CiAgICAgIDxmYW1pbHlOYW1lPkdpcmxhbmRvPC9mYW1pbHlOYW1lPgogICAgPC9jcmVhdG9yPgogICAgPGNyZWF0b3I+CiAgICAgIDxjcmVhdG9yTmFtZSBuYW1lVHlwZT0iUGVyc29uYWwiPkt1em5ldHMsIFJvbWFuPC9jcmVhdG9yTmFtZT4KICAgICAgPGdpdmVuTmFtZT5Sb21hbjwvZ2l2ZW5OYW1lPgogICAgICA8ZmFtaWx5TmFtZT5LdXpuZXRzPC9mYW1pbHlOYW1lPgogICAgPC9jcmVhdG9yPgogICAgPGNyZWF0b3I+CiAgICAgIDxjcmVhdG9yTmFtZSBuYW1lVHlwZT0iUGVyc29uYWwiPk1hcmluLCBTb25pYTwvY3JlYXRvck5hbWU+CiAgICAgIDxnaXZlbk5hbWU+U29uaWE8L2dpdmVuTmFtZT4KICAgICAgPGZhbWlseU5hbWU+TWFyaW48L2ZhbWlseU5hbWU+CiAgICA8L2NyZWF0b3I+CiAgICA8Y3JlYXRvcj4KICAgICAgPGNyZWF0b3JOYW1lIG5hbWVUeXBlPSJQZXJzb25hbCI+U3RyYcOfYnVyZ2VyLCBMdXR6PC9jcmVhdG9yTmFtZT4KICAgICAgPGdpdmVuTmFtZT5MdXR6PC9naXZlbk5hbWU+CiAgICAgIDxmYW1pbHlOYW1lPlN0cmHDn2J1cmdlcjwvZmFtaWx5TmFtZT4KICAgIDwvY3JlYXRvcj4KICA8L2NyZWF0b3JzPgogIDx0aXRsZXM+CiAgICA8dGl0bGU+QSBkZWNpc2lvbiBwcm9jZWR1cmUgZm9yIGludHVpdGlvbmlzdGljIG1vZGFsIGxvZ2ljIElTNCAoYW5kIElLNCk8L3RpdGxlPgogIDwvdGl0bGVzPgogIDxwdWJsaXNoZXI+YXJYaXY8L3B1Ymxpc2hlcj4KICA8cHVibGljYXRpb25ZZWFyPjIwMjY8L3B1YmxpY2F0aW9uWWVhcj4KICA8c3ViamVjdHM+CiAgICA8c3ViamVjdCB4bWw6bGFuZz0iZW4iIHN1YmplY3RTY2hlbWU9ImFyWGl2Ij5Mb2dpYyBpbiBDb21wdXRlciBTY2llbmNlIChjcy5MTyk8L3N1YmplY3Q+CiAgICA8c3ViamVjdCBzdWJqZWN0U2NoZW1lPSJGaWVsZHMgb2YgU2NpZW5jZSBhbmQgVGVjaG5vbG9neSAoRk9TKSI+Rk9TOiBDb21wdXRlciBhbmQgaW5mb3JtYXRpb24gc2NpZW5jZXM8L3N1YmplY3Q+CiAgPC9zdWJqZWN0cz4KICA8ZGF0ZXM+CiAgICA8ZGF0ZSBkYXRlVHlwZT0iU3VibWl0dGVkIiBkYXRlSW5mb3JtYXRpb249InYxIj4yMDI2LTA5LTIxVDE3OjE4OjIyWjwvZGF0ZT4KICAgIDxkYXRlIGRhdGVUeXBlPSJVcGRhdGVkIiBkYXRlSW5mb3JtYXRpb249InYxIj4yMDI2LTA5LTIyVDAyOjE3OjUzWjwvZGF0ZT4KICAgIDxkYXRlIGRhdGVUeXBlPSJTdWJtaXR0ZWQiIGRhdGVJbmZvcm1hdGlvbj0idjIiPjIwMjYtMTAtMDhUMTY6NTM6NDVaPC9kYXRlPgogICAgPGRhdGUgZGF0ZVR5cGU9IlVwZGF0ZWQiIGRhdGVJbmZvcm1hdGlvbj0idjIiPjIwMjYtMTAtMDlUMDE6Mjg6NDdaPC9kYXRlPgogICAgPGRhdGUgZGF0ZVR5cGU9IkF2YWlsYWJsZSIgZGF0ZUluZm9ybWF0aW9uPSJ2MSI+MjAyNi0wOTwvZGF0ZT4KICA8L2RhdGVzPgogIDxyZXNvdXJjZVR5cGUgcmVzb3VyY2VUeXBlR2VuZXJhbD0iUHJlcHJpbnQiPkFydGljbGU8L3Jlc291cmNlVHlwZT4KICA8dmVyc2lvbj4yPC92ZXJzaW9uPgogIDxyaWdodHNMaXN0PgogICAgPHJpZ2h0cyByaWdodHNVUkk9Imh0dHA6Ly9jcmVhdGl2ZWNvbW1vbnMub3JnL2xpY2Vuc2VzL2J5LzQuMC8iIHJpZ2h0c0lkZW50aWZpZXJTY2hlbWU9IlNQRFgiIHJpZ2h0c0lkZW50aWZpZXI9IkNDLUJZLTQuMCI+Q3JlYXRpdmUgQ29tbW9ucyBBdHRyaWJ1dGlvbiA0LjAgSW50ZXJuYXRpb25hbDwvcmlnaHRzPgogIDwvcmlnaHRzTGlzdD4KICA8ZGVzY3JpcHRpb25zPgogICAgPGRlc2NyaXB0aW9uIGRlc2NyaXB0aW9uVHlwZT0iQWJzdHJhY3QiPkluIHRoaXMgcGFwZXIsIHdlIHNob3cgdGhhdCB0aGUgdHdvIGludHVpdGlvbmlzdGljIG1vZGFsIGxvZ2ljcyBJUzQgYW5kIElLNCBhcmUgZGVjaWRhYmxlLiBXZSBwcm92aWRlIGEgY29uc3RydWN0aXZlIGRlY2lzaW9uIHByb2NlZHVyZSwgdGhhdCwgZ2l2ZW4gYSBmb3JtdWxhLCBwcm9kdWNlcyBlaXRoZXIgYSBwcm9vZiBzaG93aW5nIHRoZSBmb3JtdWxhIHRvIGJlIHZhbGlkIG9yIGEgZmluaXRlIGNvdW50ZXJtb2RlbCBmYWxzaWZ5aW5nIHRoZSBmb3JtdWxhLCB0aHVzIGFsc28gcHJvdmluZyB0aGUgZmluaXRlIG1vZGVsIHByb3BlcnR5IGZvciBib3RoIGxvZ2ljcy4gVGhlIG1haW4gaW5ncmVkaWVudCBvZiBvdXIgc3RyYXRlZ3kgaXMgdGhlIGludHJvZHVjdGlvbiBvZiAocG9zc2libHkgdW5zb3VuZCkgbG9vcCBydWxlcywgd2hpY2ggZW5jb2RlIHJlcGVhdGluZyBiZWhhdmlvdXIgaW4gcHJvb2Ygc2VhcmNoLiBUaGlzIHBhcGVyIGZpeGVzIGEgcHJldmlvdXMgbWlzdGFrZSBpbiBvdXIgTElDUycyMyBjb250cmlidXRpb24uPC9kZXNjcmlwdGlvbj4KICAgIDxkZXNjcmlwdGlvbiBkZXNjcmlwdGlvblR5cGU9Ik90aGVyIj5jb3JyZWN0aW9ucyBvZiBtaW5vciB0ZWNobmljYWwgaXNzdWVzIGluIHYxPC9kZXNjcmlwdGlvbj4KICA8L2Rlc2NyaXB0aW9ucz4KPC9yZXNvdXJjZT4=","url":"https://arxiv.org/abs/2609.24922","contentUrl":null,"metadataVersion":1,"schemaVersion":"http://datacite.org/schema/kernel-4","source":"mds","isActive":true,"state":"findable","reason":null,"viewCount":0,"viewsOverTime":[],"downloadCount":0,"downloadsOverTime":[],"referenceCount":0,"citationCount":0,"citationsOverTime":[],"partCount":0,"partOfCount":0,"versionCount":0,"versionOfCount":0,"created":"2026-09-22T04:35:19.000Z","registered":"2026-09-22T04:35:19.000Z","published":"2026","updated":"2026-10-09T03:25:36.000Z"},"relationships":{"client":{"data":{"id":"arxiv.content","type":"clients"}},"provider":{"data":{"id":"arxiv","type":"providers"}},"media":{"data":{"id":"10.48550/arxiv.2609.24922","type":"media"}},"references":{"data":[]},"citations":{"data":[]},"parts":{"data":[]},"partOf":{"data":[]},"versions":{"data":[]},"versionOf":{"data":[]}}}}