{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:17:14Z","timestamp":1750220234297,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T00:00:00Z","timestamp":1642118400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DFG","award":["SCHR 1118\/6-2"],"award-info":[{"award-number":["SCHR 1118\/6-2"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2022,4,30]]},"abstract":"<jats:p>\n            We establish a generic upper bound\n            <jats:sc>ExpTime<\/jats:sc>\n            for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequalities over numbers of successors, and probabilistic modal logic with polynomial inequalities over probabilities. We establish the theoretical upper bound using a type elimination algorithm. We also provide a global caching algorithm that potentially avoids building the entire exponential-sized space of candidate states, and thus offers a basis for practical reasoning. This algorithm still involves frequent fixpoint computations; we show how these can be handled efficiently in a concrete algorithm modelled on Liu and Smolka\u2019s linear-time fixpoint algorithm. Finally, we show that the upper complexity bound is preserved under adding nominals to the logic, i.e., in coalgebraic hybrid logic.\n          <\/jats:p>","DOI":"10.1145\/3501300","type":"journal-article","created":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T12:02:07Z","timestamp":1642161727000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0502-391X","authenticated-orcid":false,"given":"Clemens","family":"Kupke","sequence":"first","affiliation":[{"name":"University of Strathclyde, Glasgow, Scotland, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5832-6666","authenticated-orcid":false,"given":"Dirk","family":"Pattinson","sequence":"additional","affiliation":[{"name":"Australian National University, Canberra, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[{"name":"Friedrich-Alexander Universit\u00e4t Erlangen-N\u00fcrnberg, Erlangen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2022,1,14]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/647849.737083"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1570-2464(07)80017-6"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/2060081"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/1215128"},{"key":"e_1_3_1_6_2","first-page":"283","volume-title":"Proceedings of the European Conference on Artificial Intelligence (ECAI\u201996)","author":"Baader Franz","year":"1996","unstructured":"Franz Baader and Ulrike Sattler. 1996. Description logics with symbolic number restrictions. In Proceedings of the European Conference on Artificial Intelligence (ECAI\u201996), Wolfgang Wahlster (Ed.). Wiley, 283\u2013287."},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45114-0_7"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/381193"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3397271.3401171"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/62212.62257"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxp004"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001530100110"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_44"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2010.03.001"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2005.09.008"},{"key":"e_1_3_1_16_2","first-page":"1","article-title":"The modal logic of agency","volume":"2","author":"Elgesem Dag","year":"1997","unstructured":"Dag Elgesem. 1997. The modal logic of agency. Nordic J. Philos. Logic 2 (1997), 1\u201346.","journal-title":"Nordic J. Philos. Logic"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/174652.174658"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90060-U"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093890715"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1968.15"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.1.5"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_9"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_5"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9243-0"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_25"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.5222"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_16"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1006\/game.1999.0788"},{"key":"e_1_3_1_30_2","first-page":"235","volume-title":"Proceedings of the Conference on Advances in Modal Logic (AiML\u201910)","author":"Kupke Clemens","year":"2010","unstructured":"Clemens Kupke and Dirk Pattinson. 2010. On modal logics of linear inequalities. In Proceedings of the Conference on Advances in Modal Logic (AiML\u201910), Lev Beklemishev, Valentin Goranko, and Valentin Shehtman (Eds.). College Publications, 235\u2013255."},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22177-9_28"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00257488"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/646252.686017"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/1987171.1987195"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/3266641.3266660"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.5555\/3029848.3029925"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3322276.3322287"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1094155277"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1979.24"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2012.6378643"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/11690634_11"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.023"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.44"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85845-4_40"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/1462179.1462185"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129510000563"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.5555\/1661445.1661591"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3157055"},{"key":"e_1_3_1_52_2","first-page":"575","volume-title":"Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]","author":"Seidl Helmut","year":"2008","unstructured":"Helmut Seidl, Thomas Schwentick, and Anca Muscholl. 2008. Counting in trees. In Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], J\u00f6rg Flum, Erich Gr\u00e4del, and Thomas Wilke (Eds.). Amsterdam University Press, 575\u2013612."},{"key":"e_1_3_1_53_2","volume-title":"Complexity Results and Practical Algorithms for Logics in Knowledge Representation","author":"Tobies Stephan","year":"2001","unstructured":"Stephan Tobies. 2001. Complexity Results and Practical Algorithms for Logics in Knowledge Representation. Ph.D. Dissertation. RWTH Aachen."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3501300","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3501300","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:19Z","timestamp":1750188619000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3501300"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,14]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4,30]]}},"alternative-id":["10.1145\/3501300"],"URL":"https:\/\/doi.org\/10.1145\/3501300","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2022,1,14]]},"assertion":[{"value":"2020-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}