{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:13:34Z","timestamp":1758053614967,"version":"3.44.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Standard Description Logics (DLs) can encode quantitative aspects of an application domain through either number restrictions, which constrain the number of individuals that are in a certain relationship with an individual, or concrete domains, which can be used to assign concrete values to individuals using so-called features. These two mechanisms have been extended towards very expressive DLs, for which reasoning nevertheless remains decidable. Number restrictions have been generalized to more powerful comparisons of sets of role successors in <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathcal {ALCSCC}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>ALCSCC<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>, while the comparison of feature values of different individuals in <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathcal {ALC} (\\mathfrak {D})$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>ALC<\/mml:mi>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>D<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> has been studied in the context of <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\omega $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-admissible concrete domains <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathfrak {D}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>D<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>. In this paper, we combine both formalisms and investigate the complexity of reasoning in the thus obtained DL <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathcal {ALCOSCC}(\\mathfrak {D})$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>ALCOSCC<\/mml:mi>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>D<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>, which additionally includes the ability to refer to specific individuals by name. We show that, in spite of its high expressivity, the consistency problem for this DL is ExpTime-complete, assuming that the constraint satisfaction problem of <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathfrak {D}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>D<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> is also decidable in exponential time. It is thus not higher than the complexity of the basic DL <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathcal {ALC}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>ALC<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>. At the same time, we show that many natural extensions to this DL, including a tighter integration of the concrete domain and number restrictions, lead to undecidability.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_2","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:41Z","timestamp":1757887421000},"page":"22-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["The Expressive Power of\u00a0Description Logics with\u00a0Numerical Constraints over\u00a0Restricted Classes of\u00a0Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4049-221X","authenticated-orcid":false,"given":"Franz","family":"Baader","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8623-6465","authenticated-orcid":false,"given":"Filippo","family":"De Bortoli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"2_CR1","unstructured":"Baader, F.: A formal definition for the expressive power of knowledge representation languages. In: Proceedings of the 9th European Conference on Artificial Intelligence, ECAI 1990, pp. 53\u201358 (1990)"},{"issue":"1","key":"2_CR2","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1093\/LOGCOM\/6.1.33","volume":"6","author":"F Baader","year":"1996","unstructured":"Baader, F.: A formal definition for the expressive power of terminological knowledge representation languages. J. Log. Comput. 6(1), 33\u201354 (1996). https:\/\/doi.org\/10.1093\/LOGCOM\/6.1.33","journal-title":"J. Log. Comput."},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-66167-4_3","volume-title":"Frontiers of Combining Systems","author":"F Baader","year":"2017","unstructured":"Baader, F.: A new description logic with set constraints and cardinality constraints on role successors. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 43\u201359. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_3"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Baader, F., Bednarczyk, B., Rudolph, S.: Satisfiability and query answering in description logics with global and local cardinality constraints. In: ECAI 2020 \u2013 24th European Conference on Artificial Intelligence, pp. 616\u2013623. IOS Press (2020). https:\/\/doi.org\/10.3233\/FAIA200146","DOI":"10.3233\/FAIA200146"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Baader, F., Borgwardt, S., De Bortoli, F., Koopmann, P.: Concrete domains meet expressive cardinality restrictions in description logics. In: Barrett, C., Waldmann, U. (eds.) CADE-30: 30th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science, vol. 15943, pp.676\u2013695. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-99984-0_35","DOI":"10.1007\/978-3-031-99984-0_35"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press (2003). https:\/\/doi.org\/10.1017\/CBO9780511711787","DOI":"10.1017\/CBO9780511711787"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-030-29007-8_12","volume-title":"Frontiers of Combining Systems","author":"F Baader","year":"2019","unstructured":"Baader, F., De Bortoli, F.: On the expressive power of description logics with cardinality constraints on finite and infinite sets. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 203\u2013219. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_12"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Baader, F., De Bortoli, F.: Description logics that count, and what they can and cannot count. In: Kovacs, L., Korovin, K., Reger, G. (eds.) ANDREI-60. Automated New-era Deductive Reasoning Event in Iberia. EPiC Series in Computing, vol.\u00a068, pp. 1\u201325. EasyChair (2020). https:\/\/doi.org\/10.29007\/ltzn","DOI":"10.29007\/ltzn"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Baader, F., De\u00a0Bortoli, F.: The abstract expressive power of first-order and description logics with concrete domains. In: Proceedings of the 39th ACM\/SIGAPP Symposium on Applied Computing, SAC 2024, pp. 754\u2013761. Association for Computing Machinery, New York (2024). https:\/\/doi.org\/10.1145\/3605098.3635984","DOI":"10.1145\/3605098.3635984"},{"issue":"3","key":"2_CR10","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/3699839.3699840","volume":"24","author":"F Baader","year":"2024","unstructured":"Baader, F., De Bortoli, F.: Logics with concrete domains: first-order properties, abstract expressive power, and (un)decidability. SIGAPP Appl. Comput. Rev. 24(3), 5\u201317 (2024). https:\/\/doi.org\/10.1145\/3699839.3699840","journal-title":"SIGAPP Appl. Comput. Rev."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Baader, F., De Bortoli, F.: The Expressive Power of Description Logics with Numerical Constraints over Restricted Classes of Models (Extended Version). LTCS-Report 25-03, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit\u00e4t Dresden, Dresden, Germany (2025). https:\/\/doi.org\/10.25368\/2025.126","DOI":"10.25368\/2025.126"},{"key":"2_CR12","unstructured":"Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the 12th International Joint Conference on Artificial Intelligence, IJCAI 1991, pp. 452\u2013457. Morgan Kaufmann (1991). http:\/\/ijcai.org\/Proceedings\/91-1\/Papers\/070.pdf"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017). https:\/\/doi.org\/10.1017\/9781139025355","DOI":"10.1017\/9781139025355"},{"issue":"3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10817-022-09626-2","volume":"66","author":"F Baader","year":"2022","unstructured":"Baader, F., Rydval, J.: Using model theory to find decidable and tractable description logics with concrete domains. J. Autom. Reason. 66(3), 357\u2013407 (2022). https:\/\/doi.org\/10.1007\/s10817-022-09626-2","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"2_CR15","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/0004-3702(96)00004-5","volume":"82","author":"A Borgida","year":"1996","unstructured":"Borgida, A.: On the relative expressiveness of description logics and predicate logics. Artif. Intell. 82(1\u20132), 353\u2013367 (1996). https:\/\/doi.org\/10.1016\/0004-3702(96)00004-5","journal-title":"Artif. Intell."},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-319-49493-7_2","volume-title":"Reasoning Web: Logical Foundation of Knowledge Graph Construction and Query Answering","author":"E Botoeva","year":"2017","unstructured":"Botoeva, E., Konev, B., Lutz, C., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Inseparability and conservative extensions of description logic ontologies: a survey. In: Pan, J.Z., et al. (eds.) Reasoning Web 2016. LNCS, vol. 9885, pp. 27\u201389. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-49493-7_2"},{"key":"2_CR17","unstructured":"Calvanese, D.: Finite model reasoning in description logics. In: Aiello, L.C., Doyle, J., Shapiro, S.C. (eds.) Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR 1996), pp. 292\u2013303. Morgan Kaufmann (1996)"},{"key":"2_CR18","unstructured":"Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: Allen, J.F., Fikes, R., Sandewall, E. (eds.) Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR 1991), pp. 335\u2013346. Morgan Kaufmann (1991)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-73595-3_15","volume-title":"Automated Deduction \u2013 CADE-21","author":"V Kuncak","year":"2007","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean algebra with presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215\u2013230. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_15"},{"issue":"2","key":"2_CR20","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/S0004-3702(98)00109-X","volume":"107","author":"N Kurtonina","year":"1999","unstructured":"Kurtonina, N., de Rijke, M.: Expressiveness of concept expressions in first-order description logics. Artif. Intell. 107(2), 303\u2013333 (1999). https:\/\/doi.org\/10.1016\/S0004-3702(98)00109-X","journal-title":"Artif. Intell."},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/s10817-006-9049-7","volume":"38","author":"C Lutz","year":"2007","unstructured":"Lutz, C., Mili\u010di\u0107, M.: A tableau algorithm for description logics with concrete domains and general TBoxes. J. Autom. Reason. 38(1), 227\u2013259 (2007). https:\/\/doi.org\/10.1007\/s10817-006-9049-7","journal-title":"J. Autom. Reason."},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Lutz, C., Piro, R., Wolter, F.: Description logic TBoxes: model-theoretic characterizations and rewritability. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011), pp. 983\u2013988. IJCAI\/AAAI (2011). https:\/\/doi.org\/10.5591\/978-1-57735-516-8\/IJCAI11-169","DOI":"10.5591\/978-1-57735-516-8\/IJCAI11-169"},{"issue":"1\u20132","key":"2_CR23","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1016\/J.IC.2004.11.002","volume":"199","author":"C Lutz","year":"2005","unstructured":"Lutz, C., Sattler, U., Tendera, L.: The complexity of finite model reasoning in description logics. Inf. Comput. 199(1\u20132), 132\u2013171 (2005). https:\/\/doi.org\/10.1016\/J.IC.2004.11.002","journal-title":"Inf. Comput."},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Otto, M.: Model theoretic methods for fragments of FO and special classes of (finite) structures. In: Esparza, J., Michaux, C., Steinhorn, C. (eds.) Finite and Algorithmic Model Theory, pp. 271\u2013338. Cambridge University Press, Cambridge (2011). https:\/\/doi.org\/10.1017\/CBO9780511974960.007","DOI":"10.1017\/CBO9780511974960.007"},{"key":"2_CR25","unstructured":"Otto, M.: Graded modal logic and counting bisimulation (2023). http:\/\/arxiv.org\/abs\/1910.00039"},{"issue":"2","key":"2_CR26","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1023\/A:1005245900406","volume":"64","author":"M de Rijke","year":"2000","unstructured":"de Rijke, M.: A note on graded modal logic. Stud. Logica. 64(2), 271\u2013283 (2000). https:\/\/doi.org\/10.1023\/A:1005245900406","journal-title":"Stud. Logica."},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Rosen, E.: Modal logic over finite structures. J. Logic Lang. Inf. 6(4), 427\u2013439 (1997). https:\/\/www.jstor.org\/stable\/40181601","DOI":"10.1023\/A:1008275906015"},{"key":"2_CR28","unstructured":"van Benthem, J.: Modal correspondence theory. Ph.D. thesis, Mathematical Institute, University of Amsterdam, The Netherlands (1976)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:45Z","timestamp":1757887425000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}