{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:50:45Z","timestamp":1761965445034,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>There is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood structures. Coalgebraic logic serves as a unifying semantic and algorithmic framework for such logics. It provides uniform reasoning algorithms that are easily instantiated to particular, concretely given logics. The <jats:italic>COOL\u00a02<\/jats:italic> reasoner provides an implementation of such generic algorithms for coalgebraic modal fixpoint logics. As concrete instances, we obtain in particular reasoners for the aconjunctive and alternation-free fragments of the graded <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bc<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus and the alternating-time <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bc<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus. We evaluate the tool on standard benchmark sets for fixpoint-free graded modal logic and alternating-time temporal logic (ATL), as well as on a dedicated set of benchmarks for the graded <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bc<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_14","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"234-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["COOL 2 \u2013 A Generic Reasoner for\u00a0Modal Fixpoint Logics (System Description)"],"prefix":"10.1007","author":[{"given":"Oliver","family":"G\u00f6rlitz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0935-8602","authenticated-orcid":false,"given":"Daniel","family":"Hausmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2251-8519","authenticated-orcid":false,"given":"Merlin","family":"Humml","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5832-6666","authenticated-orcid":false,"given":"Dirk","family":"Pattinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2317-5565","authenticated-orcid":false,"given":"Simon","family":"Prucker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672\u2013713 (2002). https:\/\/doi.org\/10.1145\/585265.585270","journal-title":"J. ACM"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Calin, G., Myers, R., Pattinson, D., Schr\u00f6der, L.: CoLoSS: the coalgebraic logic satisfiability solver. In: Methods for Modalities, M4M\u20135. ENTCS, vol. 231, pp. 41\u201354. Elsevier (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.02.028","DOI":"10.1016\/j.entcs.2009.02.028"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"C\u00eerstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic $$\\mu $$-calculus. Log. Meth. Comput. Sci. 7 (2011). https:\/\/doi.org\/10.2168\/LMCS-7(3:3)2011","DOI":"10.2168\/LMCS-7(3:3)2011"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1093\/comjnl\/bxp004","volume":"54","author":"C C\u00eerstea","year":"2011","unstructured":"C\u00eerstea, C., Kurz, A., Pattinson, D., Schr\u00f6der, L., Venema, Y.: Modal logics are coalgebraic. Comput. J. 54, 31\u201341 (2011). https:\/\/doi.org\/10.1093\/comjnl\/bxp004","journal-title":"Comput. J."},{"key":"14_CR5","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s001530100110","volume":"41","author":"G D\u2019Agostino","year":"2002","unstructured":"D\u2019Agostino, G., Visser, A.: Finality regained: a coalgebraic study of Scott-sets and multisets. Arch. Math. Logic 41, 267\u2013298 (2002). https:\/\/doi.org\/10.1007\/s001530100110","journal-title":"Arch. Math. Logic"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-40537-2_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A David","year":"2013","unstructured":"David, A.: TATL: implementation of ATL tableau-based decision procedure. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS (LNAI), vol. 8123, pp. 97\u2013103. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40537-2_10"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21401-6_14","volume-title":"Automated Deduction - CADE-25","author":"A David","year":"2015","unstructured":"David, A.: Deciding $$\\sf ATL^*$$ satisfiability by tableaux. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 214\u2013228. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_14"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"issue":"4","key":"14_CR9","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1007\/s10009-022-00663-1","volume":"24","author":"J Esparza","year":"2022","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Raskin, J., Sickert, S.: From linear temporal logic and limit-deterministic B\u00fcchi automata to deterministic parity automata. Int. J. Softw. Tools Technol. Transf. 24(4), 635\u2013659 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00663-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR10","unstructured":"Friedmann, O., Lange, M.: The PGSolver collection of parity game solvers. Technical report, LMU Munich (2009)"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Friedmann, O., Lange, M.: A solver for modal fixpoint logics. In: Methods for Modalities, M4M\u20136 2009. ENTCS, vol. 262, pp. 99\u2013111 (2010). https:\/\/doi.org\/10.1016\/j.entcs.2010.04.008","DOI":"10.1016\/j.entcs.2010.04.008"},{"issue":"3","key":"14_CR12","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-014-9305-1","volume":"53","author":"B Glimm","year":"2014","unstructured":"Glimm, B., Horrocks, I., Motik, B., Stoilos, G., Wang, Z.: HermiT: an OWL 2 reasoner. J. Autom. Reason. 53(3), 245\u2013269 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9305-1","journal-title":"J. Autom. Reason."},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-14203-1_5","volume-title":"Automated Reasoning","author":"R Gor\u00e9","year":"2010","unstructured":"Gor\u00e9, R., Kupke, C., Pattinson, D., Schr\u00f6der, L.: Global caching for coalgebraic description logics. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 46\u201360. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_5"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Gor\u00e9, R., Thomson, J., Widmann, F.: An experimental comparison of theorem provers for CTL. In: Temporal Representation and Reasoning, TIME 2011, pp. 49\u201356. IEEE (2011). https:\/\/doi.org\/10.1109\/TIME.2011.16","DOI":"10.1109\/TIME.2011.16"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-319-08587-6_31","volume-title":"Automated Reasoning","author":"D Gor\u00edn","year":"2014","unstructured":"Gor\u00edn, D., Pattinson, D., Schr\u00f6der, L., Widmann, F., Wi\u00dfmann, T.: Cool \u2013 a generic reasoner for coalgebraic hybrid logics (system description). In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 396\u2013402. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_31"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"G\u00f6ttlinger, M., Schr\u00f6der, L., Pattinson, D.: The alternating-time $$\\mu $$-calculus with disjunctive explicit strategies. In: Baier, C., Goubault-Larrecq, J. (eds.) Computer Science Logic, CSL 2021. LIPIcs, vol. 183, pp. 26:1\u201326:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2021.26","DOI":"10.4230\/LIPIcs.CSL.2021.26"},{"key":"14_CR17","unstructured":"G\u00f6rlitz, O., Hausmann, D., Humml, M., Pattinson, D., Prucker, S., Schr\u00f6der, L.: Cool 2 - a generic reasoner for modal fixpoint logics (2023). https:\/\/arxiv.org\/abs\/2305.11015"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/3-540-45744-5_59","volume-title":"Automated Reasoning","author":"V Haarslev","year":"2001","unstructured":"Haarslev, V., M\u00f6ller, R.: RACER system description. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 701\u2013705. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_59"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-319-73579-5_8","volume-title":"Dynamic Logic. New Trends and Applications","author":"HH Hansen","year":"2018","unstructured":"Hansen, H.H., Kupke, C., Marti, J., Venema, Y.: Parity games and automata for game logic. In: Madeira, A., Benevides, M. (eds.) DALI 2017. LNCS, vol. 10669, pp. 115\u2013132. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73579-5_8"},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6, 512\u2013535 (1994). https:\/\/doi.org\/10.1007\/BF01211866","journal-title":"Formal Asp. Comput."},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-030-17127-8_16","volume-title":"Foundations of Software Science and Computation Structures","author":"D Hausmann","year":"2019","unstructured":"Hausmann, D., Schr\u00f6der, L.: Optimal satisfiability checking for arithmetic $$\\mu $$-calculi. In: Boja\u0144czyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 277\u2013294. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17127-8_16"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-89963-3_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Hausmann","year":"2018","unstructured":"Hausmann, D., Schr\u00f6der, L., Deifel, H.-P.: Permutation games for the weakly aconjunctive $$\\mu $$-calculus. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 361\u2013378. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_21"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Hausmann, D., Schr\u00f6der, L., Egger, C.: Global caching for the alternation-free coalgebraic $$\\mu $$-calculus. In: Concurrency Theory, CONCUR 2016. LIPIcs, vol. 59, pp. 34:1\u201334:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.34","DOI":"10.4230\/LIPIcs.CONCUR.2016.34"},{"key":"14_CR24","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983). https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","journal-title":"Theor. Comput. Sci."},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1007\/978-3-540-39910-0_30","volume-title":"Verification: Theory and Practice","author":"O Kupferman","year":"2003","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Fair equivalence relations. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 702\u2013732. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39910-0_30"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-45620-1_34","volume-title":"Automated Deduction\u2014CADE-18","author":"O Kupferman","year":"2002","unstructured":"Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded $$\\mu $$-calculus. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 423\u2013437. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_34"},{"key":"14_CR27","doi-asserted-by":"publisher","unstructured":"Kupke, C., Marti, J., Venema, Y.: Size measures and alphabetic equivalence in the $$\\mu $$-calculus. In: Baier, C., Fisman, D. (eds.) Logic in Computer Science, LICS 2022, pp. 18:1\u201318:13. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3533339","DOI":"10.1145\/3531130.3533339"},{"key":"14_CR28","unstructured":"Kupke, C., Pattinson, D.: On modal logics of linear inequalities. In: Advances in Modal Logic, AiML 2010, pp. 235\u2013255. College Publications (2010)"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Kupke, C., Pattinson, D., Schr\u00f6der, L.: Coalgebraic reasoning with global assumptions in arithmetic modal logics. ACM Trans. Comput. Log. 23(2), 11:1\u201311:34 (2022). https:\/\/doi.org\/10.1145\/3501300","DOI":"10.1145\/3501300"},{"key":"14_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K Larsen","year":"1991","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inform. Comput. 94, 1\u201328 (1991). https:\/\/doi.org\/10.1016\/0890-5401(91)90030-6","journal-title":"Inform. Comput."},{"key":"14_CR31","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on $$\\omega $$-words. Theor. Comput. Sci. 32, 321\u2013330 (1984). https:\/\/doi.org\/10.1016\/0304-3975(84)90049-5","journal-title":"Theor. Comput. Sci."},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Nalon, C., Zhang, L., Dixon, C., Hustadt, U.: A resolution prover for coalition logic. In: Mogavero, F., Murano, A., Vardi, M.Y. (eds.) Strategic Reasoning, SR 2014. EPTCS, vol. 146, pp. 65\u201373 (2014). https:\/\/doi.org\/10.4204\/EPTCS.146.9","DOI":"10.4204\/EPTCS.146.9"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/3-540-16761-7_96","volume-title":"Automata, Languages and Programming","author":"D Niwi\u0144ski","year":"1986","unstructured":"Niwi\u0144ski, D.: On fixed-point clones. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 464\u2013473. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16761-7_96"},{"key":"14_CR34","doi-asserted-by":"publisher","unstructured":"Parikh, R.: Propositional game logic. In: Foundations of Computer Science, FOCS 1983. IEEE Computer Society (1983). https:\/\/doi.org\/10.1109\/SFCS.1983.47","DOI":"10.1109\/SFCS.1983.47"},{"key":"14_CR35","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1305\/ndjfl\/1094155277","volume":"45","author":"D Pattinson","year":"2004","unstructured":"Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Logic 45, 19\u201333 (2004). https:\/\/doi.org\/10.1305\/ndjfl\/1094155277","journal-title":"Notre Dame J. Formal Logic"},{"key":"14_CR36","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1093\/logcom\/12.1.149","volume":"12","author":"M Pauly","year":"2002","unstructured":"Pauly, M.: A modal logic for coalitional power in games. J. Logic Comput. 12, 149\u2013166 (2002). https:\/\/doi.org\/10.1093\/logcom\/12.1.149","journal-title":"J. Logic Comput."},{"key":"14_CR37","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1145\/23005.23008","volume":"34","author":"D Peleg","year":"1987","unstructured":"Peleg, D.: Concurrent dynamic logic. J. ACM 34, 450\u2013479 (1987). https:\/\/doi.org\/10.1145\/23005.23008","journal-title":"J. ACM"},{"key":"14_CR38","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J Rutten","year":"2000","unstructured":"Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249, 3\u201380 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(00)00056-6","journal-title":"Theor. Comput. Sci."},{"key":"14_CR39","unstructured":"Schewe, S.: Synthesis of distributed systems. Ph.D. thesis, Universit\u00e4t des Saarlands (2008)"},{"issue":"2\u20133","key":"14_CR40","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.tcs.2007.09.023","volume":"390","author":"L Schr\u00f6der","year":"2008","unstructured":"Schr\u00f6der, L.: Expressivity of coalgebraic modal logic: the limits and beyond. Theor. Comput. Sci. 390(2\u20133), 230\u2013247 (2008). https:\/\/doi.org\/10.1016\/j.tcs.2007.09.023","journal-title":"Theor. Comput. Sci."},{"key":"14_CR41","doi-asserted-by":"publisher","unstructured":"Schr\u00f6der, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log. 10(2), 13:1\u201313:33 (2009). https:\/\/doi.org\/10.1145\/1462179.1462185","DOI":"10.1145\/1462179.1462185"},{"issue":"2","key":"14_CR42","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.websem.2007.03.004","volume":"5","author":"E Sirin","year":"2007","unstructured":"Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: a practical OWL-DL reasoner. J. Web Semant. 5(2), 51\u201353 (2007). https:\/\/doi.org\/10.1016\/j.websem.2007.03.004","journal-title":"J. Web Semant."},{"key":"14_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-28717-6_30","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"W Snell","year":"2012","unstructured":"Snell, W., Pattinson, D., Widmann, F.: Solving graded\/probabilistic modal logic via linear inequalities (system description). In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 383\u2013390. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_30"},{"key":"14_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11814771_26","volume-title":"Automated Reasoning","author":"D Tsarkov","year":"2006","unstructured":"Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: system description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292\u2013297. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_26"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:04:35Z","timestamp":1693609475000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}