Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (Extended Abstract)

Abstract

Standard description logics (DLs) can encode quantitative aspects of an application domain through either (qualified) number restrictions or concrete domain restrictions. Using qualified number restrictions, we can constrain the number of role successors belonging to a certain concept by a fixed natural number: for example, Human ⊓ (≥ 3 child.Human) ⊑ ∃eligible.TaxBreak says that a tax break is available if one has at least three children. On the other hand, concrete domain restrictions are suitable to represent a diferent type of quantitative information, where concrete objects such as numbers or strings can be assigned to individuals using partial functions (features). For example, a tax break might only be available if the annual salary is not too high. The CI Human ⊓ (≥ 3 child.Human) ⊓ ∃salary.< 100,000 ⊑ ∃eligible.TaxBreak specifies at least three children and an annual salary of less than 100,000 e as eligibility criteria for a tax break. The complexity of the concept satisfiability problem for the DL ℒ, which extends ℒ with qualified number restrictions, is the same as that of ℒ, i.e. PSpace-complete without a TBox and ExpTime-complete w.r.t. an ontology comprising a TBox and an ABox [1, 2]. This result holds for both unary and binary coding of the natural numbers occurring in number restrictions. Later, it was showed that the unrestricted use of transitive roles within number restrictions can cause undecidability in the presence of role inclusion axioms [3]. In [4], it was shown that reasoning in ℒ, which extends ℒ with very expressive counting constraints on role successors expressed in the logic QFBAPA [5], still has the same complexity as in ℒ and ℒ. In this DL, we can describe humans that have exactly as many cars as children with the concept Human ⊓ succ(|own ∩ Car| = |child ∩ Human|), without having to specify the exact numbers of cars and children. Unlike ℒ concepts, which form a fragment of first-order logic (FOL), the concept in the previous sentence cannot be expressed in FOL [ 6]. Concept satisfiability for ℒ(D), the extension of ℒ with restrictions over a concrete domain D, is decidable without a TBox if D is admissible [7], essentially requiring that satisfiability of conjunctions of constraints over the predicates of D is decidable. The presence of a TBox leads to undecidability of ℒ(D) even for rather simple instances of D [8, 9]. Decidability of concept satisfiability w.r.t. a TBox is regained by considering so-called -admissible concrete domains [10], which additionally satisfy the so-called patchwork and homomorphism -compactness properties. Moreover, reasoning in ℒ(D) remains in ExpTime if additionally the constraint satisfaction problem of D is assumed to be in ExpTime [11]. Two examples of such concrete domains are Allen's interval algebra [12] and RCC8 [13]. Using well-known notions and results from model theory, additional -admissible concrete domains were exhibited in [9, 14], for example the rational numbers with comparisons Q := (Q, <, =, >). Decidability results for ℒ(D) in the presence of CIs for concrete domains D that are not -admissible can be found in [15, 16, 17]. A simpler, but considerably more restrictive way of achieving decidability

-

is to use unary concrete domains [18].

In [ 19 ], we study ℒ(D), a combination of the DLs ℒ and ℒ(D) with -admissible concrete domains D as well as nominals (). Rather than only looking at the plain combination of these logics, we consider stronger forms of interaction between the numerical constraints of ℒ and the feature values over D. For numerical concrete domains, such as Q, we consider mixed numerical constraints that allow for the usage of concrete features directly in the QFBAPA constraints, e.g. to describe people that own more books than their age. We show, however, that this unrestricted combination easily leads to undecidability. For arbitrary -admissible concrete domains, we introduce feature roles, defined in terms of the relations holding among the feature values of two individuals, which can then be employed within QFBAPA constraints. An example is given by the feature role (salary < next salary), which connects an individual to all individuals that have a higher salary. One can use this to describe all persons that have a lower salary than at least half of their children with succ(|child ∩ (salary < next salary)| > |child ∩ (salary ≥ next salary)|) . Due to the semantics of ℒ, feature roles may only connect an individual to individuals that are also role successors. We also analyze an unrestricted variant where feature roles may connect arbitrary individuals; formally, this is obtained by taking the DL ℒ++, where constraints range over all individuals in an interpretation [ 20 ]. Lastly, we study the extension of ℒ by transitive roles. Consistency of ℒ(D). By considering ExpTime--admissible concrete domains, which are -admissible concrete domains D whose constraint satisfaction problem is decidable in exponential time, we derive the following decidability result.

Theorem 1. Let D be an ExpTime--admissible concrete domain. Then consistency checking in ℒ(D) is ExpTime-complete.

The ExpTime-hardness of this decision problem is trivially derived from the fact that ℒ(D) subsumes ℒ. The upper bound, on the other hand, is obtained by means of an algorithm based on type elimination. In this case, we use augmented types that, in addition to the standard notion of type, encode information about the concrete domain restrictions and number restrictions that must be satisfied by an individual described by a type. There are few results in the literature that determine the exact complexity of reasoning in DLs with concrete domains [ 21, 16, 17, 11 ]. Only [ 21 ] and [11] consider -admissible concrete domains, and the ExpTime-completeness result in the former is restricted to a specific temporal concrete domain. Theorem 1 extends the results of the latter from ℒ(D) to ℒ(D) and is generic since it holds for all ExpTime--admissible concrete domains. Undecidable extensions. While Theorem 1 provides a positive result, every other extension described earlier leads to undecidability, under the natural assumption that the concrete domain D is jointly diagonal (JD), i.e. that equality between elements of D can be expressed using the relations of D. In the case of , we show that undecidability holds even if we apply all the restrictions added in [ 3, 22 ] to regain decidability.

Theorem 2. Consistency in is undecidable, even if numerical constraints contain no transitive roles and no constants other than 0 or 1.

Let D be a jointly diagonal and infinite concrete domain. Then the consistency problem for ℒ++(D) TBoxes is undecidable. If D is numerical, then consistency of ℒ(D) TBoxes with mixed numerical constraints is undecidable.

The undecidability result for is obtained by a reduction from the tiling problem, similar to the one proposed in [ 3 ] for ℋ . For ℒ++(D), we show that we can reduce Hilbert’s tenth problem to consistency, by adapting the reduction used in [ 20 ] used to show that concept satisfiability in ℒ++ with inverse roles is undecidable. Finally, the presence of mixed numerical constraints leads to undecidability, since we can encode the consistency problem for ℒ(D) with a numerical concrete domain D over the natural numbers with the binary successor relation, which is known to be undecidable [14].

Reasoning with constants. Using nominals, we can internalize concept and role assertions within concept inclusions. In a similar way, we can encode predicate assertions of the form (1(1), . . . , ()) where is a relation of the concrete domain D, each is an individual and each is a feature name. An example of a predicate assertion is salary(Sam) < salary(Jane), which intuitively asserts that Jane’s salary is higher than Sam’s. On the other hand, we may want to also use feature assertions of the form (, ) to state that the -value of the individual is equal to the element of the concrete domain D. With feature assertions, we can give specific values and state, for instance, that Sam’s salary is 100,001 e with salary(Sam, 100,001). For -admissible domains D, supporting feature assertions is equivalent to support additional singleton predicates = that are not part of D, but can be used in concepts with a similar semantics, provided that D satisfies additional conditions. These conditions concern the usage of constants in constraint systems, in relation to their encoding, and are satisfied by the main known examples of ExpTime- -admissible concrete domains (Q, Allen’s relations, and RCC8) under the reasonable assumptions that all numbers are given as integer fractions in binary encoding and the constants in RCC8 refer to polygonal regions in the rational plane [ 23, 24 ]. We call the resulting structures ExpTime--admissible concrete domains with constants. We obtain the following result for homogeneous concrete domains D, i.e. where every isomorphism between finite substructures of D can be extended to an isomorphism from D to itself [14].

Theorem 3. If D is an ExpTime--admissible and homogeneous concrete domain with constants, then consistency in ℒ(D) with feature assertions and additional singleton predicates is ExpTimecomplete.

The conference paper [ 19 ] and the technical report [ 25 ] contain a detailed discussion of all the results above. While feature roles can already express a restricted form of inverse roles, in the future, we would like to investigate the decidability and complexity of ℒℐ(D) with full inverse roles, which increase the complexity of classical DLs with nominals and number restrictions to NExpTime [ 2 ]. Another avenue of research is to implement a reasoner for ℒ(D), based on a suitable tableaux algorithm [10] that needs to integrate a QFBAPA solver and a concrete domain reasoner. Currently, reasoners for DLs with non-trivial concrete domains only exist for ℒ(D) and ℰ ℒ(D) with so-called -admissible concrete domains and without feature paths [ 26 ].

Acknowledgments

This work was partially supported by DFG grant 389792660 as part of TRR 248 – CPEC, by the German Federal Ministry of Education and Research (BMBF, SCADS22B) and the Saxon State Ministry for Science, Culture and Tourism (SMWK) by funding the competence center for Big Data and AI “ScaDS.AI Dresden/Leipzig”.

Declaration on Generative AI

The author(s) have not employed any Generative AI tools. [4] F. Baader, A new description logic with set constraints and cardinality constraints on role successors, in: C. Dixon, M. Finger (Eds.), Proc. of the 11th Int. Symposium on Frontiers of Combining Systems (FroCoS’17), volume 10483 of Lecture Notes in Computer Science, SpringerVerlag, Brasília, Brazil, 2017, pp. 43–59. doi:10.1007/978-3-319-66167-4_3. [5] V. Kuncak, M. Rinard, Towards Eficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic, in: F. Pfenning (Ed.), Automated Deduction – CADE-21, volume 4603 of Lecture Notes in Computer Science, Springer Berlin Heidelberg, Berlin, Heidelberg, 2007, pp. 215–230. doi:10.1007/978-3-540-73595-3_15. [6] F. Baader, F. De Bortoli, On the expressive power of description logics with cardinality constraints on finite and infinite sets, in: A. Herzig, A. Popescu (Eds.), Frontiers of Combining Systems – 12th International Symposium, FroCoS 2019, Proceedings, volume 11715 of Lecture Notes in Computer Science, Springer, 2019, pp. 203–219. doi:10.1007/978-3-030-29007-8_12. [7] F. Baader, P. Hanschke, A scheme for integrating concrete domains into concept languages, in: J. Mylopoulos, R. Reiter (Eds.), Proceedings of the 12th International Joint Conference on Artificial Intelligence, IJCAI 1991, Morgan Kaufmann, 1991, pp. 452–457. URL: http://ijcai.org/Proceedings/ 91-1/Papers/070.pdf. [8] C. Lutz, NExpTime-complete description logics with concrete domains, ACM Transactions on

Computational Logic (TOCL) 5 (2004) 669–705. doi:10.1145/1024922.1024925. [9] F. Baader, J. Rydval, Description logics with concrete domains and general concept inclusions revisited, in: N. Peltier, V. Sofronie-Stokkermans (Eds.), Automated Reasoning – 10th International Joint Conference, IJCAR 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, Springer, 2020, pp. 413–431. doi:10.1007/978-3-030-51074-9_24. [10] C. Lutz, M. Miličić, A Tableau Algorithm for Description Logics with Concrete Domains and General TBoxes, Journal of Automated Reasoning 38 (2007) 227–259. doi:10.1007/ s10817-006-9049-7. [11] S. Borgwardt, F. De Bortoli, P. Koopmann, The precise complexity of reasoning in ℒ with -admissible concrete domains, in: L. Giordano, J. C. Jung, A. Ozaki (Eds.), Proceedings of the 37th International Workshop on Description Logics (DL 2024), volume 3739 of CEUR Workshop Proceedings, CEUR-WS.org, 2024. URL: https://ceur-ws.org/Vol-3739/paper-1.pdf. [12] J. F. Allen, Maintaining knowledge about temporal intervals, Commun. ACM 26 (1983) 832–843.

doi:10.1145/182.358434. [13] D. A. Randell, Z. Cui, A. G. Cohn, A spatial logic based on regions and connection, in: B. Nebel, C. Rich, W. R. Swartout (Eds.), Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR’92), Morgan Kaufmann, 1992, pp. 165–176. [14] F. Baader, J. Rydval, Using Model Theory to Find Decidable and Tractable Description Logics with Concrete Domains, Journal of Automated Reasoning 66 (2022) 357–407. doi:10.1007/ s10817-022-09626-2. [15] C. Carapelle, A. Turhan, Description logics reasoning w.r.t. general tboxes is decidable for concrete domains with the ehd-property, in: G. A. Kaminka, M. Fox, P. Bouquet, E. Hüllermeier, V. Dignum, F. Dignum, F. van Harmelen (Eds.), ECAI 2016 – 22nd European Conference on Artificial Intelligence, volume 285 of Frontiers in Artificial Intelligence and Applications, IOS Press, 2016, pp. 1440–1448. doi:10.3233/978-1-61499-672-9-1440. [16] N. Labai, M. Ortiz, M. Simkus, An ExpTime upper bound for ℒ with integers, in: D. Calvanese, E. Erdem, M. Thielscher (Eds.), Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, 2020, pp. 614–623. doi:10.24963/KR.2020/ 61. [17] S. Demri, K. Quaas, First steps towards taming description logics with strings, in: S. A. Gaggl, M. V. Martinez, M. Ortiz (Eds.), Logics in Artificial Intelligence – 18th European Conference, JELIA 2023, Proceedings, volume 14281 of Lecture Notes in Computer Science, Springer, 2023, pp. 322–337. doi:10.1007/978-3-031-43619-2_23. [18] I. Horrocks, U. Sattler, Ontology reasoning in the ℋ(D) description logic, in: B. Nebel (Ed.), Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI

References

[1] S. Tobies , PSPACE reasoning for graded modal logics , J. Log. Comput . 11 ( 2001 ) 85 - 106 . doi: 10 . 1093/LOGCOM/11.1.85.

[2] S. Tobies , The complexity of reasoning with cardinality restrictions and nominals in expressive description logics , J. Artif. Intell. Res . 12 ( 2000 ) 199 - 217 . doi: 10 .1613/JAIR.705.

[3] I. Horrocks , U. Sattler , S. Tobies , Practical reasoning for very expressive description logics , Log. J. IGPL 8 ( 2000 ) 239 - 263 . doi: 10 .1093/JIGPAL/8.3.239. 2001 , Morgan Kaufmann, 2001 , pp. 199 - 204 .

[19] F. Baader , S. Borgwardt , F. De Bortoli, P. Koopmann, Concrete domains meet expressive cardinality restrictions in description logics , in: C. Barrett , U. Waldmann (Eds.), Automated Deduction - CADE 30, volume 15943 of Lecture Notes in Artificial Intelligence , Stuttgart, Germany, 2025 , pp. 676 - 695 . doi: 10 .1007/978-3- 031 -99984-0_ 35 .

[20] F. Baader , B. Bednarczyk , S. Rudolph , Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints , in: ECAI 2020 , IOS Press, 2020 , pp. 616 - 623 . doi: 10 .3233/FAIA200146.

[21] C. Lutz , The complexity of description logics with concrete domains , Ph.D. thesis , RWTH Aachen University, Germany, 2002 . URL: http://sylvester.bth.rwth-aachen.de/dissertationen/2002/042/ index.htm.

[22] V. Gutiérrez-Basulto , Y. A. Ibáñez-García , J. C. Jung , Number restrictions on transitive roles in description logics with nominals , in: S. Singh, S. Markovitch (Eds.), Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence , AAAI Press, 2017 , pp. 1121 - 1127 . doi: 10 .1609/AAAI. V31I1.10678.

[23] P. Jonsson , Constants and finite unary relations in qualitative constraint reasoning , Artificial Intelligence 257 ( 2018 ) 1 - 23 . doi: 10 .1016/j.artint. 2017 . 12 .003.

[24] S. Li , W. Liu , S. Wang , Qualitative constraint satisfaction problems: An extended framework with landmarks , Artificial Intelligence 201 ( 2013 ) 32 - 58 . doi: 10 .1016/j.artint. 2013 . 05 .006.

[25] F. Baader , S. Borgwardt , F. De Bortoli, P. Koopmann, Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (Extended Version) , 2025 . arXiv: 2505 . 21103 .

[26] C. Alrabbaa , F. Baader , S. Borgwardt , P. Koopmann , A. Kovtunova , Combining proofs for description logic and concrete domain reasoning , in: A. Fensel , A. Ozaki , D. Roman , A . Soylu (Eds.), Rules and Reasoning - 7th International Joint Conference, RuleML+RR 2023 , Proceedings , volume 14244 of Lecture Notes in Computer Science, Springer, 2023 , pp. 54 - 69 . doi: 10 .1007/ 978-3- 031 -45072- 3 _ 4 .