{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:39:39Z","timestamp":1753889979911,"version":"3.41.2"},"reference-count":31,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,4,27]],"date-time":"2012-04-27T00:00:00Z","timestamp":1335484800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We investigate the complexity of the model checking problem for\nintuitionistic and modal propositional logics over transitive Kripke models.\nMore specific, we consider intuitionistic logic IPC, basic propositional logic\nBPL, formal propositional logic FPL, and Jankov's logic KC. We show that the\nmodel checking problem is P-complete for the implicational fragments of all\nthese intuitionistic logics. For BPL and FPL we reach P-hardness even on the\nimplicational fragment with only one variable. The same hardness results are\nobtained for the strictly implicational fragments of their modal companions.\nMoreover, we investigate whether formulas with less variables and additional\nconnectives make model checking easier. Whereas for variable free formulas\noutside of the implicational fragment, FPL model checking is shown to be in\nLOGCFL, the problem remains P-complete for BPL.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:3)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":1,"title":["Intuitionistic implication makes model checking hard"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Martin","family":"Mundhenk","sequence":"first","affiliation":[]},{"given":"Felix","family":"Weiss","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,4,27]]},"reference":[{"key":"10.2168\/LMCS-8(2:3)2012_bo93","doi-asserted-by":"crossref","unstructured":"G. S. Boolos.The Logic of Provability. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511625183"},{"key":"10.2168\/LMCS-8(2:3)2012_Bou04","unstructured":"F. Bou. Complexity of strict implication. InAdvances in Modal Logic 5, pages 1-16, 2005."},{"key":"10.2168\/LMCS-8(2:3)2012_bus87","doi-asserted-by":"crossref","unstructured":"S. R. Buss. The Boolean formula value problem is in ALOGTIME. InProc. 19th STOC, pages 123-131. ACM Press, 1987.","DOI":"10.1145\/28395.28409"},{"key":"10.2168\/LMCS-8(2:3)2012_Chagrov85","unstructured":"A. V. Chagrov. On the complexity of propositional logics. InComplexity Problems in Mathematical Logic, pages 80-90. Kalinin State University, 1985. In Russian."},{"key":"10.2168\/LMCS-8(2:3)2012_ChagrovR02","unstructured":"A. V. Chagrov and M. N. Rybakov. How many variables does one need to prove PSPACE-hardness of modal logics. InAdvances in Modal Logic, volume 4, pages 71-82, 2002."},{"key":"10.2168\/LMCS-8(2:3)2012_chkost81","doi-asserted-by":"crossref","unstructured":"A. K. Chandra, D. Kozen, and L. J. Stockmeyer. Alternation.Journal of the Association for Computing Machinery, 28:114-133, 1981.","DOI":"10.1145\/322234.322243"},{"key":"10.2168\/LMCS-8(2:3)2012_DeJonghJSL1970","unstructured":"D. H. de Jongh. The maximality of the intuitionistic predicate calculus with respect to Heyting's arithmetic.The Journal of Symbolic Logic, 36:606, 1970."},{"key":"10.2168\/LMCS-8(2:3)2012_RHJ10","doi-asserted-by":"crossref","unstructured":"G. R. R. de Lavalette, A. Hendriks, and D. H. de Jongh. Intuitionistic implication without disjunction.Journal of Logic and Computation. To appear, available at http:\/\/dx.doi.org\/10.1093\/logcom\/exq058.","DOI":"10.1093\/logcom\/exq058"},{"issue":"24","key":"10.2168\/LMCS-8(2:3)2012_DL59","first-page":"250","volume":"14","author":"M. Dummett and E. Lemmon","year":"1959","journal-title":"Zeitschrift f\u00fcr Mathematik"},{"issue":"2","key":"10.2168\/LMCS-8(2:3)2012_filad79","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. J. Fischer and R. E. Ladner","year":"1979","journal-title":"Journal of Computer and Systems Sciences"},{"key":"10.2168\/LMCS-8(2:3)2012_grhoru95","doi-asserted-by":"crossref","unstructured":"R. Greenlaw, H. J. Hoover, and W. L. Ruzzo.Limits to Parallel Computation: P-Completeness Theory. Oxford University Press, New York, 1995.","DOI":"10.1093\/oso\/9780195085914.001.0001"},{"issue":"1","key":"10.2168\/LMCS-8(2:3)2012_JH93","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1093\/logcom\/3.1.63","volume":"3","author":"J. Hudelmaier","year":"1993","journal-title":"Journal of Logic and Computation"},{"key":"10.2168\/LMCS-8(2:3)2012_JT07","doi-asserted-by":"crossref","unstructured":"A. Jakoby and T. Tantau. Logspace algorithms for computing shortest and longest paths in series-parallel graphs. InFSTTCS, volume 4855 ofLecture Notes in Computer Science, pages 216-227, 2007.","DOI":"10.1007\/978-3-540-77050-3_18"},{"key":"10.2168\/LMCS-8(2:3)2012_Kripke63ML","first-page":"67","volume":"9","author":"S. A. Kripke","year":"1963","journal-title":"Zeitschrift f\u00fcr Mathematik"},{"issue":"3","key":"10.2168\/LMCS-8(2:3)2012_lad77","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. E. Ladner","year":"1977","journal-title":"SIAM J. Comput."},{"key":"10.2168\/LMCS-8(2:3)2012_McKinseyTarski44","doi-asserted-by":"crossref","first-page":"141","DOI":"10.2307\/1969080","volume":"45","author":"J. C. C. McKinsey and A. Tarski","year":"1944","journal-title":"Annals of Mathematics"},{"key":"10.2168\/LMCS-8(2:3)2012_MW-RP10","doi-asserted-by":"crossref","unstructured":"M. Mundhenk and F. Wei\u00df. The complexity of model checking for intuitionistic logics and their modal companions. InProc. 4th Int. Workshop on Reachability Problems, volume 6227 ofLNCS, pages 146-160. Springer, 2010.","DOI":"10.1007\/978-3-642-15349-5_10"},{"key":"10.2168\/LMCS-8(2:3)2012_MW-STACS11","unstructured":"M. Mundhenk and F. Wei\u00df. The model checking problem for intuitionistic propositional logic with one variable isACi-complete. InProc. 28th STACS, volume 9 of LIPIcs, pages 368-379. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2011."},{"key":"10.2168\/LMCS-8(2:3)2012_pap94","unstructured":"C. H. Papadimitriou.Computational Complexity. Addison-Wesley, Reading, MA, 1994."},{"key":"10.2168\/LMCS-8(2:3)2012_KR-presonal11","unstructured":"K. Reinhardt. Model checking forPrL0on linear frames is in ACi, 2011. Personal communication."},{"key":"10.2168\/LMCS-8(2:3)2012_Rybakov06","unstructured":"M. N. Rybakov. Complexity of intuitionistic and Visser's basic and formal logics in finitely many variables. InAdvances in Modal Logic 6, pages 393-411. College Publications, 2006."},{"issue":"3","key":"10.2168\/LMCS-8(2:3)2012_sicl85","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. Sistla and E. Clarke","year":"1985","journal-title":"J. ACM"},{"key":"10.2168\/LMCS-8(2:3)2012_spaan93","unstructured":"E. Spaan.Complexity of Modal Logics. PhD thesis, Department of Mathematics and Computer Science, University of Amsterdam, 1993."},{"key":"10.2168\/LMCS-8(2:3)2012_stat79","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R. Statman","year":"1979","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"10.2168\/LMCS-8(2:3)2012_sve00","first-page":"95","volume":"4","author":"V. Svejdar","year":"2000","journal-title":"Nordic Journal of Philosophical Logic"},{"issue":"8","key":"10.2168\/LMCS-8(2:3)2012_svejdar03a","doi-asserted-by":"crossref","first-page":"763","DOI":"10.1007\/s00153-003-0180-4","volume":"42","author":"V. Svejdar","year":"2003","journal-title":"Arch. Math. Log."},{"issue":"7","key":"10.2168\/LMCS-8(2:3)2012_svejdar03","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1007\/s00153-003-0179-x","volume":"42","author":"V. Svejdar","year":"2003","journal-title":"Arch. Math. Log."},{"key":"10.2168\/LMCS-8(2:3)2012_Tar38","doi-asserted-by":"crossref","first-page":"103","DOI":"10.4064\/fm-31-1-103-134","volume":"31","author":"A. Tarski","year":"1938","journal-title":"Fundamenta Mathematicae"},{"issue":"4","key":"10.2168\/LMCS-8(2:3)2012_Urq74","doi-asserted-by":"crossref","first-page":"661","DOI":"10.2307\/2272850","volume":"39","author":"A. Urquhart","year":"1974","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(2:3)2012_dal04","doi-asserted-by":"crossref","unstructured":"D. van Dalen.Logic and Structure. Springer, Berlin, Heidelberg, 4th edition, 2004.","DOI":"10.1007\/978-3-540-85108-0"},{"key":"10.2168\/LMCS-8(2:3)2012_visser80","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/BF01874706","volume":"40","author":"A. Visser","year":"1980","journal-title":"Studia Logica"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1160\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1160\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:05:07Z","timestamp":1681243507000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1160"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,27]]},"references-count":31,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:3)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1107.1963","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1107.1963","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,4,27]]},"article-number":"1160"}}