{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T20:44:36Z","timestamp":1783111476733,"version":"3.54.6"},"reference-count":29,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,6,26]],"date-time":"2023-06-26T00:00:00Z","timestamp":1687737600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,6,26]],"date-time":"2023-06-26T00:00:00Z","timestamp":1687737600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,6,26]]},"DOI":"10.1109\/lics56636.2023.10175684","type":"proceedings-article","created":{"date-parts":[[2023,7,14]],"date-time":"2023-07-14T17:18:23Z","timestamp":1689355103000},"page":"1-13","source":"Crossref","is-referenced-by-count":7,"title":["Intuitionistic S4 is decidable"],"prefix":"10.1109","author":[{"given":"Marianna","family":"Girlando","sequence":"first","affiliation":[{"name":"University of Amsterdam,Amsterdam,Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roman","family":"Kuznets","sequence":"additional","affiliation":[{"name":"TU Wien,Vienna,Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sonia","family":"Marin","sequence":"additional","affiliation":[{"name":"University of Birmingham,Birmingham,UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marianela","family":"Morales","sequence":"additional","affiliation":[{"name":"Inria Saclay,Palaiseau,France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lutz","family":"Stra\u00dfburger","sequence":"additional","affiliation":[{"name":"Inria Saclay,Palaiseau,France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_9"},{"key":"ref12","first-page":"87","article-title":"Finite model property for some intuitionistic modal logics","volume":"30","author":"hasimoto","year":"2001","journal-title":"Bulletin of the Section of Logic"},{"key":"ref15","author":"kleene","year":"1952","journal-title":"Introduction to Metamathematics"},{"key":"ref14","article-title":"Untersuchungen zum Prädikatenkalkül","volume":"23","author":"ketonen","year":"1944","journal-title":"Annales Academiae Scientiarum Fennicae Series A I"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.42"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470643"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.06.007"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-018-0636-1"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-012-0061-7"},{"key":"ref18","article-title":"On the algebra of structural contexts","author":"lamarche","year":"2001","journal-title":"Mathematical Structures in Computer Science"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-934613-04-0.50032-6"},{"key":"ref23","first-page":"329","article-title":"Logische Untersuchungen über die Grundlagen der Mathematik","volume":"iii","author":"ono","year":"1938","journal-title":"Journal of the Faculty of Science Imperial University of Tokyo section I"},{"key":"ref26","article-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","author":"simpson","year":"1994","journal-title":"PhD thesis"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.2977\/prims\/1195189814"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exab020"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-005-2267-3"},{"key":"ref21","first-page":"97","article-title":"On some calculi of modal logic","volume":"98","author":"minc","year":"1971","journal-title":"Proceedings of the Steklov Institute of Mathematics"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717"},{"key":"ref27","first-page":"209","article-title":"Cut elimination in nested sequents for intuitionistic modal logics","author":"stra\u00dfburger","year":"2013","journal-title":"FOSSACS 2013"},{"key":"ref29","first-page":"168","article-title":"Intuitionistic modal logics as fragments of classical bimodal logics","author":"wolter","year":"1999","journal-title":"Logic at Work"},{"key":"ref8","first-page":"179","article-title":"Axiomatizations for some intuitionistic modal logics","volume":"42","author":"servi","year":"1984","journal-title":"Rendiconti del Seminario Matematico - PoliTO"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.2307\/2273953"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1122038925"},{"key":"ref4","article-title":"Modular focused proof systems for intuitionistic modal logics","author":"chaudhuri","year":"2016","journal-title":"FSCD 2016"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-009-0137-3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-011-0254-7"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29198-7_6"}],"event":{"name":"2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","location":"Boston, MA, USA","start":{"date-parts":[[2023,6,26]]},"end":{"date-parts":[[2023,6,29]]}},"container-title":["2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10175635\/10175671\/10175684.pdf?arnumber=10175684","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,1]],"date-time":"2023-08-01T17:59:20Z","timestamp":1690912760000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10175684\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,26]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/lics56636.2023.10175684","relation":{},"subject":[],"published":{"date-parts":[[2023,6,26]]}}}