The Precise Complexity of Reasoning in π’œβ„’π’ž with πœ”-Admissible Concrete Domains Stefan Borgwardt1 , Filippo De Bortoli1,2 and Patrick Koopmann3 1 TU Dresden, Institute of Theoretical Computer Science Dresden, Germany 2 Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI) Dresden/Leipzig, Germany 3 Vrije Universiteit Amsterdam, Department of Computer Science Amsterdam, The Netherlands Abstract Concrete domains have been introduced in the context of Description Logics to allow references to qualitative and quantitative values. In particular, the class of πœ”-admissible concrete domains, which includes Allen’s interval algebra, the region connection calculus (RCC8), and the rational numbers with ordering and equality, has been shown to yield extensions of π’œβ„’π’ž for which concept satisfiability w.r.t. a general TBox is decidable. In this paper, we present an algorithm based on type elimination and use it to show that deciding the consistency of an π’œβ„’π’ž(D) ontology is ExpTime-complete if the concrete domain D is πœ”-admissible and its constraint satisfaction problem is decidable in exponential time. While this allows us to reason with concept and role assertions, we also investigate feature assertions 𝑓 (π‘Ž, 𝑐) that can specify a constant 𝑐 as the value of a feature 𝑓 for an individual π‘Ž. We show that, under conditions satisfied by all known πœ”-admissible domains, we can add feature assertions without affecting the complexity. Keywords Description Logics, Concrete Domains, Reasoning, Complexity, Type Elimination 1. Introduction Reasoning about numerical attributes of objects is a core requirement of many applications. For this reason, Description Logics (DLs) that integrate reasoning over an abstract domain of knowledge with references to values drawn from a concrete domain have already been investigated for over 30 years [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]. In this setting, DLs are extended by concrete features that are interpreted as partial functions mapping abstract domain elements to concrete values, such as the feature diastolic that describes the diastolic blood pressure of a person. Using concrete domain restrictions we can then describe constraints over these features and state, e.g. that all patients have a diastolic blood pressure that is lower than their systolic blood pressure, by adding the concept inclusion Patient βŠ‘ βˆƒdiastolic, systolic.< to the ontology. More interestingly, we can use feature paths to compare the feature values of different individuals: the inclusion ⊀ βŠ‘ βˆ€hasChild age, age.< states that children are always younger than their parents. Unfortunately, dealing with feature paths in DLs is very challenging and often leads to undecid- ability [2, 11, 9], which is why restrictive conditions on the concrete domains were introduced to regain decidability. An approach inspired from research on constraint satisfaction is based on πœ”- admissibility [5], which requires certain compositionality properties for finite and countable sets of constraints. This enables the composition of full models from local solutions of sets of concrete domain constraints. Being quite restrictive, at first only two examples of πœ”-admissible concrete domains were DL 2024: 37th International Workshop on Description Logics, June 18–21, 2024, Bergen, Norway $ stefan.borgwardt@tu-dresden.de (S. Borgwardt); filippo.de_bortoli@tu-dresden.de (F. De Bortoli); p.k.koopmann@vu.nl (P. Koopmann) Β€ https://lat.inf.tu-dresden.de/~stefborg (S. Borgwardt); https://lat.inf.tu-dresden.de/~debortoli (F. De Bortoli); https://pkoopmann.github.io (P. Koopmann)  0000-0003-0924-8478 (S. Borgwardt); 0000-0002-8623-6465 (F. De Bortoli); 0000-0001-5999-2583 (P. Koopmann) Β© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings known, namely Allen’s interval algebra and the region connection calculus (RCC8). Recently, the conditions of πœ”-admissibility were investigated in more detail, and it was shown that πœ”-admissible concrete domains can be obtained from finitely bounded homogeneous structures [9]. This class includes the rational numbers Q := (Q, <, =, >) with ordering and equality, and is closed under union and certain types of product [9]. Despite these extensive investigations, the precise complexity of reasoning using description logics with concrete domains has been established only for a few special cases so far [2, 7, 8, 10]. These results have been obtained by automata-based techniques, and yield decidability or tight complexity bounds for cases where the concrete domain is not πœ”-admissible, such as the ordered integers (Z, <, =, >) [8] or the set of strings over a finite alphabet with a prefix relation [10]. In contrast, the goal of this paper is to derive a tight complexity bound for ontology consistency in the extension of π’œβ„’π’ž with any πœ”-admissible concrete domain. Using an algorithm based on type elimination, we establish that this decision problem is ExpTime-complete under the assumption that the concrete domain D is πœ”-admissible and that its constraint satisfaction problem (CSP) is decidable in exponential time. The latter condition holds for all finitely bounded homogeneous structures (including the three examples from above), since their CSP is guaranteed to be in NP and in some cases, e.g. for Q, is decidable in polynomial time. Additionally, we consider predicate and feature assertions. These allow us to constrain values of features associated to named individuals, e.g. to write <(age(mary), age(bob)) to state that Mary is younger than Bob, or to specify a constant value of a feature for a named individual, e.g. using systolic(mary, 122) to state that Mary’s systolic blood pressure equals 122. We prove that consistency in the presence of predicate assertions can always be reduced in polynomial time to consistency without predicate assertions. For feature assertions, we show that this holds if we consider homogeneous πœ”- admissible concrete domains, which again is the case for the three concrete domains from above. Finally, we show that supporting feature assertions is equivalent to supporting singleton predicates of the form =𝑐 for a constant 𝑐 in the concrete domain. Omitted proofs of the results presented in the text can be found in [12]. 2. Preliminaries Concrete Domains. As usual for DLs, we adopt the term concrete domain to refer to a relational structure D = (𝐷, 𝑃1𝐷 , 𝑃2𝐷 , . . . ) over a non-empty, countable relational signature {𝑃1 , 𝑃2 , . . . }, where 𝐷 is a non-empty set, and each predicate 𝑃 has an associated arity π‘˜ ∈ N and is interpreted by a relation 𝑃 𝐷 βŠ† π·π‘˜ . An example is the structure Q := (Q, <, =, >) over the rational numbers Q with standard binary order and equality relations. Given a countably infinite set 𝑉 of variables, a constraint system over 𝑉 is a set C of constraints 𝑃 (𝑣1 , . . . , π‘£π‘˜ ), where 𝑣1 , . . . , π‘£π‘˜ ∈ 𝑉 and 𝑃 is a π‘˜-ary predicate of D. We denote by 𝑉 (C) the set of variables that occur in C. The constraint system C is satisfiable if there is a homomorphism β„Ž : 𝑉 (C) β†’ 𝐷 that satisfies every constraint in C, i.e. 𝑃 (𝑣1 , . . . , π‘£π‘˜ ) ∈ C implies (β„Ž(𝑣1 ), . . . , β„Ž(π‘£π‘˜ )) ∈ 𝑃 𝐷 . We then call β„Ž a solution of C. The constraint satisfaction problem for D, denoted CSP(D), is the decision problem asking whether a finite constraint system C over D is satisfiable. The problem CSP(Q) is in P, since satisfiability can be reduced to <-cycle detection; for example, the 3-clique {π‘₯1 < π‘₯2 , π‘₯2 < π‘₯3 , π‘₯3 < π‘₯1 } (using infix notation for <) is unsatisfiable over Q. To ensure that reasoning in the extension of π’œβ„’π’ž with concrete domain restrictions is decidable, we impose further properties on D regarding its relations and the compositionality of its CSP for finite and countable constraint systems. We say that D is a patchwork if it satisfies the following conditions:1 JEPD for all π‘˜ β‰₯ 1, either D has no π‘˜-ary relation, or π·π‘˜ is partitioned by all π‘˜-ary relations; JD there is a quantifier-free, equality-free first-order formula over the signature of D that defines the equality relation = between two elements of D; 1 [5] originally used only JEPD (jointly exhaustive, pairwise disjoint) and AP (amalgamation property). JD (jointly diagonal) was later added by [9]. AP if B, C are constraint systems and 𝑃 (𝑣1 , . . . , π‘£π‘˜ ) ∈ B iff 𝑃 (𝑣1 , . . . , π‘£π‘˜ ) ∈ C holds for all 𝑣1 , . . . , π‘£π‘˜ ∈ 𝑉 (B) ∩ 𝑉 (C) and all π‘˜-ary predicates 𝑃 over D, then B and C are satisfiable iff B βˆͺ C is satisfiable. If D is a patchwork, we call a constraint system C complete if, for all π‘˜ ∈ N, either D has no π‘˜-ary predicates, or for all 𝑣1 , . . . , π‘£π‘˜ ∈ 𝑉 (C) there is exactly one π‘˜-ary predicate 𝑃 over D such that 𝑃 (𝑣1 , . . . , π‘£π‘˜ ) ∈ C. The concrete domain D is homomorphism πœ”-compact if a countable constraint system C over D is satisfiable whenever every finite constraint system Cβ€² βŠ† C is satisfiable. We now introduce our definition of ExpTime-πœ”-admissible concrete domains, which differs from the definitions of πœ”-admissibility [5, 9] in that we require CSP(D) to be decidable in exponential time instead of simply decidable. Definition 1. A concrete domain D is ExpTime-πœ”-admissible if β€’ D has a finite signature, β€’ D is a patchwork, β€’ D is homomorphism πœ”-compact, and β€’ CSP(D) is decidable in exponential time. Requiring the signature of D to be finite is necessary to ensure decidability of π’œβ„’π’ž(D) [9]. In Sec- tion 4, we will also consider concrete domains D that are homogeneous, that is, every isomorphism between finite substructures of D can be extended to an isomorphism from D to itself. All properties we have defined here are satisfied by the three examples of Allen’s interval relations, RCC8, and Q, as they are finitely bounded homogeneous structures, which are πœ”-admissible and have CSPs whose complexity is at most NP (see [9] for details). Ontologies with Concrete Domain Constraints. We assume the reader to be familiar with the standard description logic π’œβ„’π’ž [13]. To use a concrete domain D in π’œβ„’π’ž axioms, we introduce a set of concrete features NF , where each 𝑓 ∈ NF is interpreted as a partial function 𝑓 ℐ : βˆ†β„ β†’ 𝐷 in an interpretation ℐ. A feature path is of the form π‘Ÿ1 . . . π‘Ÿπ‘› 𝑓 , where π‘Ÿ1 , . . . , π‘Ÿπ‘› ∈ NR are role names and 𝑓 ∈ NF . The semantics of such a path is given by a function (π‘Ÿ1 . . . π‘Ÿπ‘› 𝑓 )ℐ (𝑑) := 𝑓 ℐ (𝑒) | (𝑑, 𝑒) ∈ π‘Ÿ1ℐ ∘ Β· Β· Β· ∘ π‘Ÿπ‘›β„ and 𝑓 ℐ (𝑒) is defined {οΈ€ }οΈ€ that assigns to each domain element the set of all 𝑓 -values of elements 𝑒 reachable via the role chain π‘Ÿ1 . . . π‘Ÿπ‘› (which may be empty if there is no such 𝑒, or if 𝑓 ℐ (𝑒) is always undefined). In a slight abuse of notation, we allow the case where 𝑛 = 0, i.e. 𝑓 can be seen as both a feature and a feature path, with slightly different, but equivalent semantics (that is, a partial function vs. a set-valued function that may produce either a singleton set or the empty set). π’œβ„’π’ž(D) concepts are defined similarly to π’œβ„’π’ž concepts, but can additionally use the following concept constructor: A concrete domain restriction (or simply CD-restriction) is of the form βˆƒπ‘1 , . . . , π‘π‘˜ .𝑃 or βˆ€π‘1 , . . . , π‘π‘˜ .𝑃 , where 𝑝1 , . . . , π‘π‘˜ are feature paths and 𝑃 is a π‘˜-ary predicate, with the semantics (βˆƒπ‘1 , . . . , π‘π‘˜ .𝑃 )ℐ := 𝑑 ∈ βˆ†β„ | there are 𝑐𝑖 ∈ 𝑝ℐ𝑖 (𝑑) for 𝑖 = 1, . . . , π‘˜ s.t. (𝑐1 , . . . , π‘π‘˜ ) ∈ 𝑃 𝐷 , {οΈ€ }οΈ€ (βˆ€π‘1 , . . . , π‘π‘˜ .𝑃 )ℐ := 𝑑 ∈ βˆ†β„ | if 𝑐𝑖 ∈ 𝑝ℐ𝑖 (𝑑) for 𝑖 = 1, . . . , π‘˜, then (𝑐1 , . . . , π‘π‘˜ ) ∈ 𝑃 𝐷 . {οΈ€ }οΈ€ An π’œβ„’π’ž(D) ontology π’ͺ = π’œ βˆͺ 𝒯 consists of an ABox π’œ and a TBox 𝒯 over π’œβ„’π’ž(D) concepts. Note that we explicitly consider π’œβ„’π’ž(D) and not π’œβ„’π’žβ„±(D), i.e. we do not allow functional roles, in contrast to other definitions from the literature [1, 5]. In the literature, feature paths are either restricted to contain only functional roles, or to have a length of at most 2, (compare with [2, 5]). Consequently, we restrict ourselves to feature paths of length ≀ 2, that is, assume that they are of the form 𝑓 or π‘Ÿπ‘“ . We are not aware of any work that considers feature paths over non-functional roles of length longer than 2, and leave the investigation of this case for future work. Without loss of generality, we can assume that universal CD-restrictions are not used in concepts, because we can express βˆ€π‘1 , . . . , π‘π‘˜ .𝑃 as Β¬βˆƒπ‘1 , . . . , π‘π‘˜ .𝑃1 βŠ“ Β· Β· Β· βŠ“ Β¬βˆƒπ‘1 , . . . , π‘π‘˜ .π‘ƒπ‘š , where 𝑃1 , . . . , π‘ƒπ‘š are all π‘˜-ary predicates of D except for 𝑃 (the union of these predicates is equivalent to the complement of 𝑃 due to JEPD, and there are only finitely many of them since the signature is assumed to be finite). We can additionally assume that concepts do not contain value restrictions βˆ€π‘Ÿ.𝐢 or disjunctions 𝐢 βŠ” 𝐷 since they can be expressed using only negation, conjunction and existential restriction. 3. Consistency in π’œβ„’π’ž(D) Let now D be a fixed ExpTime-πœ”-admissible concrete domain, π’ͺ = π’œ βˆͺ 𝒯 be an π’œβ„’π’ž(D) ontology, and β„³ be the set of all subconcepts appearing in π’ͺ and their negations. For the type elimination algorithm, we start by defining the central notion of types, which is standard. Definition 2. A set 𝑑 βŠ† β„³ is a type w.r.t. π’ͺ if it satisfies the following properties: β€’ if 𝐢 βŠ‘ 𝐷 ∈ 𝒯 and 𝐢 ∈ 𝑑, then 𝐷 ∈ 𝑑; β€’ if ⊀ ∈ β„³, then ⊀ ∈ 𝑑; β€’ if ¬𝐷 ∈ β„³, then 𝐷 ∈ 𝑑 iff ¬𝐷 ∈ / 𝑑; β€’ if 𝐷 βŠ“ 𝐷′ ∈ β„³, then 𝐷 βŠ“ 𝐷′ ∈ 𝑑 iff 𝐷 ∈ 𝑑 and 𝐷′ ∈ 𝑑. Given a model ℐ of π’ͺ and an individual 𝑑 ∈ βˆ†β„ , the type of 𝑑 w.r.t. π’ͺ is the set 𝑑ℐ (𝑑) := 𝐢 ∈ β„³ | 𝑑 ∈ 𝐢 ℐ . {οΈ€ }οΈ€ Clearly, 𝑑ℐ (𝑑) satisfies the four conditions required to be a type w.r.t. π’ͺ. We use this connection between individuals and types to define augmented types that represent the relationship between an individual, its role successors, and the CD-restrictions that ought to be satisfied. Hereafter, let 𝑛ex be the number of existential restrictions βˆƒπ‘Ÿ.𝐢 in β„³, and 𝑛cd the number of CD-restrictions βˆƒπ‘1 , . . . , π‘π‘˜ .𝑃 in β„³. The maximal arity of predicates 𝑃 occurring in β„³ is denoted by 𝑛ar , and we define 𝑛π’ͺ := 𝑛ex + 𝑛cd Β· 𝑛ar . Intuitively, each non-negated existential restriction in a type needs a successor (and associated type) to be realized, while CD-restrictions may require 𝑛ar role successors to fulfill a certain constraint. Therefore, 𝑛π’ͺ is an upper bound on the number of successors needed to satisfy all the non-negated restrictions occurring in a type 𝑑 w.r.t. π’ͺ. Given a type 𝑑0 , we define a constraint system associated with a sequence of types 𝑑1 , . . . , 𝑑𝑛π’ͺ representing the role successors of a domain element with type 𝑑0 . This system contains a variable 𝑓 𝑖 for each feature 𝑓 of an individual with type 𝑑𝑖 in order to express the relevant CD-restrictions. Concrete features that are not represented in this system can remain undefined since their values are irrelevant for satisfying the CD-restrictions. Definition 3. A local system for a type 𝑑0 w.r.t. a sequence of types 𝑑1 , . . . , 𝑑𝑛π’ͺ is a complete constraint system C for which there exists a successor function succ : NR (π’ͺ) β†’ 𝒫({1, . . . , 𝑛π’ͺ }), such that, for all βˆƒπ‘1 , . . . , π‘π‘˜ .𝑃 ∈ β„³, the following condition holds: βˆƒπ‘1 , . . . , π‘π‘˜ .𝑃 ∈ 𝑑0 iff there is 𝑃 (𝑣1 , . . . , π‘£π‘˜ ) ∈ C for some variables 𝑣1 , . . . , π‘£π‘˜ such that {οΈƒ 𝑓 0 if 𝑝𝑖 = 𝑓 , or 𝑣𝑖 = 𝑓 𝑗 if 𝑝𝑖 = π‘Ÿπ‘“ and 𝑗 ∈ succ(π‘Ÿ). We use a sequence instead of a set of types for the role successors, since there can be TBoxes that require the existence of two successors with the same type that only differ in their feature values. For example, for the consistent ontology π’ͺ := {⊀ βŠ‘ βˆƒπ‘Ÿπ‘“, π‘Ÿπ‘“.<} over Q = (Q, <, =, >), we have β„³ = {⊀, ¬⊀, βˆƒπ‘Ÿπ‘“, π‘Ÿπ‘“.<, Β¬βˆƒπ‘Ÿπ‘“, π‘Ÿπ‘“.<}, and the only type is 𝑑 = {⊀, βˆƒπ‘Ÿπ‘“, π‘Ÿπ‘“.<}. Any π‘Ÿ-successors witnessing βˆƒπ‘Ÿπ‘“, π‘Ÿπ‘“.< for an element in a model of π’ͺ have the same type 𝑑. However, we cannot express the restriction on their 𝑓 -values by the (unsatisfiable) constraint <(𝑓 𝑑 , 𝑓 𝑑 ), but need to consider two copies 𝑑1 , 𝑑2 of 𝑑 to get the (satisfiable) constraint <(𝑓 1 , 𝑓 2 ). To merge the local systems associated to types of adjacent elements in a model, we introduce the following operation. For two local systems C, Cβ€² , the merged system C ◁𝑖 Cβ€² is obtained as the union of C and Cβ€² where we identify all features with index 𝑖 in C with those of index 0 in Cβ€² , while keeping β€² the remaining variables separate. Formally, we first replace all variables 𝑓 𝑗 in Cβ€² by fresh variables 𝑓 𝑗 β€² and subsequently replace the variables 𝑓 0 in Cβ€² by 𝑓 𝑖 . Definition 4. An augmented type for π’ͺ is a tuple t := (𝑑0 , . . . , 𝑑𝑛π’ͺ , Ct ) where 𝑑0 , . . . , 𝑑𝑛π’ͺ are types for π’ͺ and Ct is a local system for 𝑑0 w.r.t. 𝑑1 , . . . , 𝑑𝑛π’ͺ . The root of t is root(t) := 𝑑0 . The augmented type t is locally realizable if Ct has a solution and if there exists a successor function succt for Ct s.t. for all concepts βˆƒπ‘Ÿ.𝐢 ∈ β„³, it holds that βˆƒπ‘Ÿ.𝐢 ∈ root(t) iff there is 𝑖 ∈ succt (π‘Ÿ) such that 𝐢 ∈ 𝑑𝑖 . An augmented type tβ€² then patches t at 𝑖 ∈ succt (π‘Ÿ) if root(tβ€² ) = 𝑑𝑖 and the system Ct ◁𝑖 Ctβ€² has a solution. A set of augmented types T patches the locally realizable t if, for every role name π‘Ÿ and every 𝑖 ∈ succt (π‘Ÿ), there is a tβ€² ∈ T that patches t at 𝑖. For the ontology π’ͺ introduced above, we have 𝑛π’ͺ = 2 since β„³ only contains one CD-restriction over a binary predicate. Using infix notation, all augmented types t = (𝑑, 𝑑, 𝑑, Ct ) for π’ͺ are such that Ct contains the constraints 𝑓 𝑖 = 𝑓 𝑖 for 𝑖 = 0, 1, 2, and either 𝑓 1 < 𝑓 2 or 𝑓 2 < 𝑓 1 . There are augmented types t that are not locally realizable, for instance if Ct contains 𝑓 0 = 𝑓 1 , 𝑓 0 = 𝑓 2 , and 𝑓 1 < 𝑓 2 . On the other hand, there is a locally realizable augmented type using the constraints 𝑓 0 < 𝑓 1 , 𝑓 1 < 𝑓 2 , and 𝑓 0 < 𝑓 2 , which can patch itself both at 𝑖 ∈ {1, 2}. To additionally handle named individuals and concept and role assertions, we introduce a structure tπ’œ that describes all ABox individuals and their connections simultaneously, similar to the common notion of precompletion. The associated constraint system Cπ’œ now uses variables 𝑓 π‘Ž,𝑖 indexed with individual names π‘Ž in addition to numbers 𝑖. Definition 5. An ABox type for π’ͺ is a tuple tπ’œ := (tπ‘Ž )π‘ŽβˆˆNI (π’œ) , π’œπ‘… , Cπ’œ , where tπ‘Ž are augmented (οΈ€ )οΈ€ types, π’œπ‘… is a set of role assertions over NI (π’œ) and NR (π’ͺ), and Cπ’œ is a complete and satisfiable constraint system such that, for every π‘Ž ∈ NI (π’œ), β€’ for every concept assertion 𝐢(π‘Ž) ∈ π’œ, we have 𝐢 ∈ root(tπ‘Ž ); β€’ for every role assertion π‘Ÿ(π‘Ž, 𝑏) ∈ π’œ, we have π‘Ÿ(π‘Ž, 𝑏) ∈ π’œπ‘… ; β€’ for every Β¬βˆƒπ‘Ÿ.𝐢 ∈ root(tπ‘Ž ) and π‘Ÿ(π‘Ž, 𝑏) ∈ π’œπ‘… , we have 𝐢 ∈ / root(t𝑏 ); 𝑗1 π‘—π‘˜ π‘Ž,𝑗1 π‘Ž,π‘—π‘˜ β€’ for every 𝑃 (𝑓1 , . . . , π‘“π‘˜ ) ∈ Ctπ‘Ž , we have 𝑃 (𝑓1 , . . . , π‘“π‘˜ ) ∈ Cπ’œ ; β€’ for every Β¬βˆƒπ‘1 , . . . , π‘π‘˜ .𝑃 ∈ root(tπ‘Ž ), there can be no 𝑃 (𝑣1 , . . . , π‘£π‘˜ ) ∈ Cπ’œ with ⎧ π‘Ž,0 if 𝑝 = 𝑓 , βŽ¨π‘“ βŽͺ 𝑖 𝑣𝑖 = 𝑓 𝑏,0 if 𝑝𝑖 = π‘Ÿπ‘“ and π‘Ÿ(π‘Ž, 𝑏) ∈ π’œπ‘… , or βŽͺ ⎩ π‘Ž,𝑗 𝑓 if 𝑝𝑖 = π‘Ÿπ‘“ and 𝑗 ∈ succtπ‘Ž (π‘Ÿ); Positive occurrences of existential role or CD-restrictions in the ABox type do not need to be handled, as these are satisfied by anonymous successors described in the augmented types tπ‘Ž . 3.1. The Type Elimination Algorithm Algorithm 1 uses the introduced notions to check consistency of π’ͺ. Lemma 6 (Soundness). If Algorithm 1 returns consistent, then π’ͺ is consistent. Proof. Assume that T and t𝐴 = ((tπ‘Ž )π‘ŽβˆˆNI (π’œ) , π’œπ‘… , Cπ’œ ) are obtained after a successful run of the elimi- nation algorithm. We use them to define a forest-shaped interpretation ℐ that is a model of π’ͺ. The domain of this model consists of pairs (π‘Ž, 𝑀), where π‘Ž ∈ NI designates a tree-shaped part of ℐ whose structure is given by the words 𝑀 over the alphabet Ξ£ := T Γ— {0, . . . , 𝑛π’ͺ }. A pair (t, 𝑖) ∈ Ξ£ describes Algorithm 1 Elimination algorithm for consistency of π’œβ„’π’ž(D) ontologies Input: An π’œβ„’π’ž(D) ontology π’ͺ = π’œ βˆͺ 𝒯 Output: consistent if π’ͺ is consistent, and inconsistent otherwise 1: β„³ ← all subconcepts occurring in π’ͺ and their negations 2: T ← all augmented types for π’ͺ 3: while there is t ∈ T that is not locally realizable or not patched by T do 4: T ← T βˆ– {t} 5: if there is an ABox type tπ’œ for π’ͺ with tπ‘Ž ∈ T for all π‘Ž ∈ NI (π’œ) then 6: return consistent 7: else 8: return inconsistent an augmented type and the position relative to the restriction that this augmented type fulfills w.r.t. its parent in the tree. For a word 𝑀 ∈ Ξ£+ , we define end(𝑀) := t if (t, 𝑗) occurs at the last position of 𝑀 for some 𝑗 ∈ {0, . . . , 𝑛π’ͺ }. We start defining the domain of ℐ by βˆ†0 := {(π‘Ž, π‘€π‘Ž ) | π‘Ž ∈ NI (π’œ), π‘€π‘Ž := (tπ‘Ž , 0)}. Observe that π‘€π‘Ž ∈ Ξ£, since tπ‘Ž ∈ T. Assuming that βˆ†π‘š is defined, we define βˆ†π‘š+1 based on βˆ†π‘š , and subsequently construct the domain of ℐ as the union of all sets βˆ†π‘š . Given (π‘Ž, 𝑀) ∈ βˆ†π‘š with end(𝑀) = t, we observe that t must have a successor function succt s.t. for every 𝑖 ∈ succt (π‘Ÿ), there is an augmented type u𝑖 ∈ T patching t at 𝑖, as otherwise t would have been eliminated from T. We use these augmented types to define βˆ†π‘š+1 π‘Ÿ [π‘Ž, 𝑀] := {(π‘Ž, 𝑀 Β· (u𝑖 , 𝑖)) | 𝑖 ∈ succt (π‘Ÿ)} to then obtain ⋃︁ {οΈ€ βˆ†π‘š+1 := βˆ†π‘š βˆͺ βˆ†π‘š+1 [π‘Ž, 𝑀] | (π‘Ž, 𝑀) ∈ βˆ†π‘š and π‘Ÿ ∈ NR }οΈ€ π‘Ÿ and set βˆ†β„ := π‘š . The interpretation of individual, concept, and role names over ℐ is given by ⋃︀ π‘šβˆˆN βˆ† π‘Žβ„ := (π‘Ž, π‘€π‘Ž ), 𝐴ℐ := (π‘Ž, 𝑀) ∈ βˆ†β„ | end(𝑀) = t and 𝐴 ∈ root(t) , {οΈ€ }οΈ€ π‘Ÿβ„ := ((π‘Ž, π‘€π‘Ž ), (𝑏, 𝑀𝑏 )) | π‘Ÿ(π‘Ž, 𝑏) ∈ π’œπ‘… βˆͺ {οΈ€ }οΈ€ ((π‘Ž, 𝑀), (π‘Ž, 𝑀′ )) | (π‘Ž, 𝑀) ∈ βˆ†π‘š and (π‘Ž, 𝑀′ ) ∈ βˆ†π‘š+1 [π‘Ž, 𝑀] with π‘š ∈ N . {οΈ€ }οΈ€ π‘Ÿ Defining the interpretation of feature names in ℐ requires more work. Given (π‘Ž, 𝑀) ∈ βˆ†β„ with end(𝑀) = t, let Cπ‘Ž,𝑀 be the constraint system obtained by replacing every variable 𝑓 0 in Ct with 𝑓 π‘Ž,𝑀 and every other variable 𝑓 𝑖 in Ct with 𝑓 π‘Ž,𝑒 , where 𝑒 ∈ Ξ£+ is the unique word of the form 𝑀 Β· (tβ€² , 𝑖) for which (π‘Ž, 𝑒) ∈ βˆ†β„ . Correspondingly, let C0π’œ be the result of replacing all variables 𝑓 π‘Ž,0 in Cπ’œ by 𝑓 π‘Ž,π‘€π‘Ž and 𝑓 π‘Ž,𝑖 by 𝑓 π‘Ž,𝑒 , where 𝑒 is the unique word of the form π‘€π‘Ž Β· (tβ€² , 𝑖) for which (π‘Ž, 𝑒) ∈ βˆ†β„ . For π‘š ∈ N, let Cπ‘š be the union of C0π’œ and all constraint systems Cπ‘Ž,𝑀 for which (π‘Ž, 𝑀) ∈ βˆ†π‘š . The proofs of the following claims can be found in [12]. Claim 1. For every π‘š ∈ N, the constraint system Cπ‘š has a solution. Using this claim, we show how to define an interpretation of feature names for ℐ. Let Cℐ be the union of all systems Cπ‘š for π‘š ∈ N. Every finite system B βŠ† Cℐ is also a subsystem of Cπ‘š for some π‘š ∈ N. Since Cπ‘š has a solution, it follows that B has a solution. Every finite subsystem of Cℐ has a solution; since D has the homomorphism πœ”-compactness property, we infer that Cℐ has a solution β„Žβ„ . Using this solution, we define for every feature name 𝑓 the interpretation 𝑓 ℐ (π‘Ž, 𝑀) := β„Žβ„ (𝑓 π‘Ž,𝑀 ) if 𝑓 π‘Ž,𝑀 occurs in Cℐ , and leave it undefined otherwise. Claim 2. If 𝐢 ∈ β„³ and (π‘Ž, 𝑀) ∈ βˆ†β„ with end(𝑀) = t, then 𝐢 ∈ root(t) iff (π‘Ž, 𝑀) ∈ 𝐢 ℐ . By this claim and Definition 2, we know that ℐ is a model of 𝒯 . By Definition 5 we obtain that for each 𝐢(π‘Ž) ∈ π’œ, we have 𝐢 ∈ root(tπ‘Ž ), and thus π‘Žβ„ = (π‘Ž, π‘€π‘Ž ) = (π‘Ž, (tπ‘Ž , 0)) ∈ 𝐢 ℐ . Similarly, whenever π‘Ÿ(π‘Ž, 𝑏) ∈ π’œ, then π‘Ÿ(π‘Ž, 𝑏) ∈ π’œπ‘… , and thus (π‘Žβ„ , 𝑏ℐ ) = ((π‘Ž, π‘€π‘Ž ), (𝑏, 𝑀𝑏 )) ∈ π‘Ÿβ„ by the construction of ℐ. Therefore, we conclude that ℐ is also a model of π’œ, and thus of π’ͺ. Lemma 7 (Completeness). If π’ͺ is consistent, then Algorithm 1 returns consistent. Proof. Let ℐ be a model of π’ͺ and define the set 𝑇ℐ of all types that are realized in ℐ, that is, 𝑇ℐ := 𝑑ℐ (𝑑) | 𝑑 ∈ βˆ†β„ . {οΈ€ }οΈ€ Given that ℐ is a model of π’ͺ, every element of 𝑇ℐ is a type according to Definition 2. Using the elements of 𝑇ℐ , we construct a set Tℐ := {tℐ (𝑑) | 𝑑 ∈ βˆ†β„ } of augmented types. For any domain element 𝑑 ∈ βˆ†β„ , we build the augmented type tℐ (𝑑) = (𝑑0 , . . . , 𝑑𝑛π’ͺ , C𝑑 ) as follows. First, we set 𝑑0 := 𝑑ℐ (𝑑) ∈ 𝑇ℐ . Assuming that βˆƒπ‘Ÿπ‘– .𝐢𝑖 ∈ β„³ for 𝑖 = 1, . . . , 𝑛ex , we select types 𝑑1 , . . . , 𝑑𝑛ex to add to t that realize the (possibly negated) existential role restrictions occurring in 𝑑0 . If βˆƒπ‘Ÿπ‘– .𝐢𝑖 ∈ 𝑑0 , then we can select 𝑑𝑖 as the type of an π‘Ÿ-successor 𝑑′ of 𝑑 such that 𝑑′ ∈ 𝐢𝑖ℐ ; otherwise, we pick 𝑑𝑖 as the type of an arbitrary element in βˆ†β„ . Next, we assume that βˆƒπ‘π‘–1 , . . . , π‘π‘–π‘˜ .𝑃𝑖 ∈ β„³ for 𝑖 = 1, . . . , 𝑛cd and define the function off(𝑖, 𝑗) := 𝑛ex + (𝑖 βˆ’ 1) Β· 𝑛ar + 𝑗 to be able to refer to the 𝑗-th path in the 𝑖-th CD-restriction above. We select types 𝑑off(𝑖,1) , . . . , 𝑑off(𝑖,𝑛ar ) that realize the (possibly negated) existential CD-restrictions occurring in 𝑑0 ℐ for 𝑖 = 1, . . . , 𝑛cd . If βˆƒπ‘π‘–1 , . . . , π‘π‘–π‘˜ .𝑃𝑖 ∈ 𝑑0 , then there exist values 𝑣𝑗𝑖 ∈ (𝑝𝑖𝑗 ) (𝑑) for 𝑗 = 1, . . . , π‘˜ such that (𝑣1𝑖 , . . . , π‘£π‘˜π‘– ) ∈ 𝑃 𝐷 . If 𝑝𝑗 = π‘Ÿπ‘“ holds for some feature name 𝑓 and some role name π‘Ÿ, let 𝑑off(𝑖,𝑗) be the type of an π‘Ÿ-successor 𝑑′ of 𝑑 such that 𝑣𝑗𝑖 = 𝑓 ℐ (𝑑). For every 𝑗 = 1, . . . , 𝑛ar for which 𝑑off(𝑖,𝑗) has not been selected this way, let 𝑑off(𝑖,𝑗) be the type of an arbitrary individual in βˆ†β„ . Similarly, if / 𝑑0 then we set 𝑑off(𝑖,𝑗) be the type of an arbitrary individual in βˆ†β„ for 𝑗 = 1, . . . , 𝑛ar . βˆƒπ‘π‘–1 , . . . , π‘π‘–π‘˜ .𝑃𝑖 ∈ The two processes described in the two previous paragraphs yield a sequence of types 𝑑1 , . . . , 𝑑𝑛π’ͺ that occur in 𝑇ℐ and can thus be associated to individuals 𝑑1 , . . . , 𝑑𝑛π’ͺ ∈ βˆ†β„ . Using these individuals, we define the local system associated to (οΈ€ our augmented (οΈ€type tℐ (𝑑). First, we define the constraint system 𝑖1 π‘–π‘˜ )οΈ€ C𝑑 that contains the constraint 𝑃 𝑓1 , . . . , π‘“π‘˜ iff 𝑓1 (𝑑𝑖1 ), . . . , π‘“π‘˜ (π‘‘π‘–π‘˜ ) ∈ 𝑃 𝐷 for all 𝑖1 , . . . , π‘–π‘˜ ∈ ℐ ℐ )οΈ€ {0, . . . , 𝑛π’ͺ }. We associate to this constraint system a successor function succ𝑑 that assigns to π‘Ÿ ∈ NR all 𝑖 ∈ {1, . . . , 𝑛π’ͺ } for which 𝑑𝑖 is an π‘Ÿ-successor of 𝑑. This concludes our definition of tℐ (𝑑) for 𝑑 ∈ βˆ†β„ , and thus of Tℐ . Claim 3. Every augmented type in Tℐ is locally realizable and patched in Tℐ . Therefore, no augmented type t ∈ Tℐ is eliminated during a run of Algorithm 1, and so Tℐ βŠ† T. We further deduce that T cannot become empty, since 𝑇ℐ is non-empty. Using Tℐ together with our model ℐ of π’ͺ we derive an ABox type tβ„π’œ = (tπ‘Ž )π‘ŽβˆˆNI (π’œ) , π’œπ‘… , Cπ’œ for π’ͺ. We define each tπ‘Ž , π‘Ž ∈ NI (π’œ), as (οΈ€ )οΈ€ tπ‘Ž := tℐ (π‘Žβ„ ) ∈ Tℐ . Assuming that π‘‘π‘Ž,𝑖 is the domain element used to establish the 𝑖-th type in tπ‘Ž for 𝑖 ∈ {0, . . . , 𝑛π’ͺ }, we define the constraint system Cπ’œ s.t. 𝑃 (𝑓1π‘Ž1 ,𝑖1 , . . . , π‘“π‘˜π‘Žπ‘˜ ,π‘–π‘˜ ) ∈ Cπ’œ iff (𝑓1ℐ (π‘‘π‘Ž1 ,𝑖1 ), . . . , π‘“π‘˜β„ (π‘‘π‘Žπ‘˜ ,π‘–π‘˜ )) ∈ 𝑃 𝐷 . Finally, we define the set π’œπ‘… to consist of all role assertions π‘Ÿ(π‘Ž, 𝑏) for which π‘Ž, 𝑏 ∈ NI (π’œ), π‘Ÿ ∈ NR (π’ͺ), and (π‘Žβ„ , 𝑏ℐ ) ∈ π‘Ÿβ„ . Claim 4. The object tβ„π’œ is an ABox type for π’ͺ with tπ‘Ž ∈ Tℐ for all π‘Ž ∈ NI (π’œ). Thus, there is a suitable ABox type for π’ͺ, and Algorithm 1 returns consistent. We can show in a standard way that Algorithm 1 runs in exponential time w.r.t. π’ͺ and obtain the following theorem (a detailed proof can be found in [12]). Theorem 8. Let D be an ExpTime-πœ”-admissible concrete domain. Then, the consistency problem for π’œβ„’π’ž(D) ontologies is ExpTime-complete. 4. Concrete Domain Assertions Beside using concrete domain restrictions on the concept level, we may want to use feature and predicate assertions in the ABox to either assign a specific value of a feature to some individual or directly constraint the values of features of different individuals. Formally, a feature assertion is of the form 𝑓 (π‘Ž, 𝑐), where 𝑓 ∈ NF , π‘Ž ∈ NI , and 𝑐 ∈ (οΈ€ 𝐷, and it is satisfied )οΈ€ by an interpretation ℐ if 𝑓 ℐ (π‘Žβ„ ) = 𝑐. Predicate assertions are of the form 𝑃 𝑓1 (π‘Ž1 ), . . . , π‘“π‘˜ (π‘Žπ‘˜ ) , where 𝑃 is a π‘˜-ary relation over (οΈ€ ℐ D and 𝑓𝑖 ∈ NF)οΈ€, π‘Žπ‘– ∈ NI for 𝑖 = 1, . . . , π‘˜. An interpretation ℐ satisfies such an assertion if 𝑓1 (π‘Žβ„1 ), . . . , π‘“π‘˜β„ (π‘Žβ„π‘˜ ) ∈ 𝑃 𝐷 . In our setting, we can simulate predicate assertions using concept and role assertions, which leads to the following result. Theorem 9. For any ExpTime-πœ”-admissible concrete domain D, ontology consistency in π’œβ„’π’ž(D) with predicate assertions is ExpTime-complete. Proof. First, we show how to simulate CD-restrictions of the form βˆƒπ‘“.⊀D that describe all individuals 𝑑 in ℐ for which 𝑓 ℐ (𝑑) is defined. Although ⊀D may not be a predicate of D, by JEPD and the fact that the signature of D is non-empty and finite, ⊀D can be expressed as the disjunction of some π‘˜-ary predicates 𝑃1 , . . . , π‘ƒπ‘š . This implies that for every 𝑑 ∈ 𝐷 there is exactly one π‘˜-ary predicate 𝑃𝑖 such that (𝑑, . . . , 𝑑) ∈ 𝑃𝑖𝐷 . Thus, we can write βˆƒπ‘“.⊀D equivalently as βˆƒπ‘“, . . . , 𝑓.𝑃1 βŠ” Β· Β· Β· βŠ” βˆƒπ‘“, . . . , 𝑓.π‘ƒπ‘š , where each restriction βˆƒπ‘“, . . . , 𝑓.𝑃𝑖 repeats 𝑓 for π‘˜ times. Let now π’ͺ = π’œ βˆͺ 𝒯 be an π’œβ„’π’ž(D) ontology with predicate assertions. We introduce a fresh individual name π‘Ž* and fresh role names π‘Ÿπ‘Ž for all individual names π‘Ž ∈ NI (π’ͺ). The ontology π’ͺβ€² is then obtained from (οΈ€ π’ͺ by adding the role )οΈ€ assertions π‘Ÿπ‘Ž (π‘Ž , π‘Ž) for all π‘Ž ∈ NI (π’ͺ), and replacing all predicate * assertions 𝑃 𝑓1 (π‘Ž1 ), . . . , π‘“π‘˜ (π‘Žπ‘˜ ) in π’œ by the concept assertions (βˆƒπ‘“1 .⊀D )(π‘Ž1 ), . . . , (βˆƒπ‘“π‘˜ .⊀D )(π‘Žπ‘˜ ), and (βˆ€π‘Ÿπ‘Ž1 𝑓1 , . . . , π‘Ÿπ‘Žπ‘˜ π‘“π‘˜ .𝑃 )(π‘Ž* ). Any model ℐ of π’ͺβ€² satisfies (𝑐1 , . . . , π‘π‘˜ ) ∈ 𝑃 𝐷 for all possible values 𝑐𝑖 ∈ (π‘Ÿπ‘Žπ‘– 𝑓𝑖 )ℐ , and thus in particular for 𝑐𝑖 = 𝑓𝑖ℐ (π‘Žβ„π‘– ), which shows that ℐ is also a model of π’ͺ. Conversely, from every model ℐ of π’ͺ we obtain a model of π’ͺβ€² by choosing an arbitrary element 𝑑* ∈ βˆ†β„ for the interpretation of π‘Ž* and adding (𝑑* , π‘Žβ„ ) to the interpretation of π‘Ÿπ‘Ž for every individual name π‘Ž. Feature assertions can also be simulated under certain conditions. For concrete domains that contain singleton predicates =𝑐 with (=𝑐 )𝐷 = {𝑐} βŠ† 𝐷, we can express any feature assertion 𝑓 (π‘Ž, 𝑐) using the concept assertion (βˆƒπ‘“.=𝑐 )(π‘Ž). However, due to its finite signature, D can only contain finitely many such predicates, and hence the feature assertions are restricted by the chosen concrete domain. Due to the JD and JEPD conditions, it turns out that adding feature assertions is actually equivalent to adding singleton predicates in the following sense. Here, an additional singleton predicate =𝑐 is one that is not part of D, but otherwise can be used in an ontology with the same semantics as defined above; the proof can be found in [12]. Theorem 10. For an πœ”-admissible concrete domain D, ontology consistency in π’œβ„’π’ž(D) with additional singleton predicates can be polynomially reduced to ontology consistency in π’œβ„’π’ž(D) with feature assertions. If we additionally require D to be homogeneous, then we can show that arbitrary feature assertions can already be expressed in ordinary π’œβ„’π’ž(D) ontologies. Theorem 11. For an ExpTime-πœ”-admissible homogeneous concrete domain D, ontology consistency in π’œβ„’π’ž(D) with feature assertions is ExpTime-complete. Proof. Due to Theorem 9, it suffices to provide a reduction to ontology consistency with predicate assertions. Let π’ͺ = π’œ βˆͺ 𝒯 be an π’œβ„’π’ž(D) ontology containing feature assertions. Let π’œβ€² be the ABox containing all concept and role assertions from π’œ and, in addition, all predicate assertions 𝑃 (𝑓1 (π‘Ž1 ), . . . , π‘“π‘˜ (π‘Žπ‘˜ )) ∈ π’œβ€² for all combinations of feature assertions 𝑓𝑖 (π‘Žπ‘– , 𝑐𝑖 ) ∈ π’œ with 𝑖 = 1, . . . , π‘˜ for which (𝑐1 , . . . , π‘π‘˜ ) ∈ 𝑃 𝐷 holds. The size of π’œβ€² is polynomial in the input, since the signature of D is fixed. It is easy to see that every model of π’ͺ is also a model of π’ͺβ€² := π’œβ€² βˆͺ 𝒯 . Conversely, let ℐ be a model of π’ͺβ€² and let Dπ’œ , Dℐ be the finite substructures of D over the domains π·π’œ := {𝑐 | 𝑓 (π‘Ž, 𝑐) ∈ π’œ} and 𝐷ℐ := {𝑓 ℐ (π‘Ž) | 𝑓 (π‘Ž, 𝑐) ∈ π’œ}, respectively. By definition of π’œβ€² and JEPD, we know that 𝑓1ℐ (π‘Žβ„1 ), . . . , π‘“π‘˜β„ (π‘Žβ„π‘˜ ) ∈ 𝑃 𝐷 iff (𝑐1 , . . . , π‘π‘˜ ) ∈ (οΈ€ )οΈ€ 𝑃 𝐷 , for all combinations of feature assertions 𝑓𝑖 (π‘Žπ‘– , 𝑐𝑖 ) in π’œ. By JD, this in particular implies that 𝑓1ℐ (π‘Žβ„1 ) = 𝑓2ℐ (π‘Žβ„2 ) iff 𝑓1 (π‘Ž1 , 𝑐), 𝑓2 (π‘Ž2 , 𝑐) ∈ π’œ for some value 𝑐 ∈ 𝐷, which means that the two substructures have the same number of elements. Moreover, by the first equivalence, the mapping 𝑓 ℐ (π‘Žβ„ ) ↦→ 𝑐 for all 𝑓 (π‘Ž, 𝑐) ∈ π’œ is an isomorphism between Dℐ and Dπ’œ . Since D is homogeneous, there exists an isomorphism β„Ž : 𝐷 β†’ 𝐷 such that β„Ž(𝑓 ℐ (π‘Žβ„ )) = 𝑐 if 𝑓 (π‘Ž, 𝑐) ∈ π’œ. Consequently, we β€² define ℐ β€² from ℐ by changing the interpretation of feature names to 𝑓 ℐ (𝑑) := β„Ž(𝑓 ℐ (𝑑)) iff this value β€² is defined for 𝑓 ∈ NF and 𝑑 ∈ βˆ†β„ . Since β„Ž is an isomorphism, we have 𝐢 ℐ = 𝐢 ℐ for all concepts 𝐢, including CD restrictions, which shows that ℐ β€² is a model of 𝒯 and all concept and role assertions β€² β€² in π’œ. Moreover, it also satisfies all feature assertions 𝑓 (π‘Ž, 𝑐) ∈ π’œ since 𝑓 ℐ (π‘Žβ„ ) = β„Ž(𝑓 ℐ (π‘Žβ„ )) = 𝑐 by construction. Together with Theorem 10, this also shows that one can use arbitrary singleton equality predicates in π’œβ„’π’ž(D) ontologies over a homogeneous concrete domain D, even if D contains only finitely many singleton predicates (or none). 5. Conclusion In this paper, we revisited the problem of reasoning in π’œβ„’π’ž(D) with an πœ”-admissible concrete do- main D, first addressed in [5]. There, it was conjectured that concept satisfiability w.r.t. a TBox is ExpTime-complete, provided that CSP(D) is decidable in exponential time. Using an approach based on type elimination, we successfully proved this conjecture. In addition, we integrated ABox reasoning and showed that reasoning w.r.t. an π’œβ„’π’ž(D) ontology where one can refer to specific values via feature assertions is also ExpTime-complete, if in addition to the above D is an πœ”-admissible homogeneous structure. The main examples of πœ”-admissible concrete domains from the literature fulfill this require- ment as they are (reducts of) finitely bounded homogeneous structures [9], and so we obtain insights into the complexity of reasoning with extensions of π’œβ„’π’ž by concrete domain restrictions ranging over Allen’s interval algebra, the region connection calculus RCC8, the rational numbers with ordering and equality, and disjoint combinations of those domains. By extending the type elimination algorithm proposed in this paper appropriately, we believe that it is possible to show that decidability is preserved in extensions of π’œβ„’π’ž(D) such as π’œβ„’π’žβ„(D), where inverse roles are allowed in both role and concrete domain restrictions (so that we can write, e.g. βˆ€hasChildβˆ’ age, hasChild age.>), and π’œβ„’π’žπ’¬(D), which supports qualified number restrictions. We also plan to use this type elimination approach as a starting point in our investigations of different inference problems, for instance signature-based abduction [14] for π’œβ„’π’ž(D) ontologies and abstract definability for π’œβ„’π’ž(D) TBoxes, i.e. checking whether their abstract expressive power [15] can be defined in π’œβ„’π’ž. 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". The authors would like to thank Jakub Rydval for his help in understanding the properties of finitely bounded homogeneous structures. References [1] 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. Sydney, Australia, August 24-30, 1991, Morgan Kaufmann, 1991, pp. 452–457. URL: http://ijcai.org/Proceedings/91-1/Papers/070.pdf. [2] C. Lutz, The complexity of description logics with concrete domains, Ph.D. thesis, RWTH Aachen University, Germany, 2002. URL: http://nbn-resolving.org/urn:nbn:de:hbz:82-opus-3032. [3] C. Lutz, Description logics with concrete domains - A survey, in: P. Balbiani, N. Suzuki, F. Wolter, M. Zakharyaschev (Eds.), Advances in Modal Logic 4, King’s College Publications, 2002, pp. 265–296. URL: http://www.aiml.net/volumes/volume4/Lutz.ps. [4] F. Baader, S. Brandt, C. Lutz, Pushing the EL envelope, in: L. P. Kaelbling, A. Saffiotti (Eds.), IJCAI-05, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Professional Book Center, 2005, pp. 364–369. URL: http://ijcai.org/Proceedings/05/Papers/0372.pdf. [5] 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. [6] A. Artale, V. Ryzhikov, R. Kontchakov, DL-Lite with attributes and datatypes, in: L. D. Raedt, C. Bessiere, D. Dubois, P. Doherty, P. Frasconi, F. Heintz, P. J. F. Lucas (Eds.), ECAI 2012 - 20th European Conference on Artificial Intelligence, volume 242 of Frontiers in Artificial Intelligence and Applications, IOS Press, 2012, pp. 61–66. doi:10.3233/978-1-61499-098-7-61. [7] C. Carapelle, A.-Y. Turhan, Description Logics Reasoning w.r.t. General TBoxes Is Decidable for Concrete Domains with the EHD-Property, in: ECAI 2016, IOS Press, 2016, pp. 1440–1448. doi:10.3233/978-1-61499-672-9-1440. [8] N. Labai, M. Ortiz, M. Ε imkus, An ExpTime Upper Bound for ALC with Integers, Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning 17 (2020) 614–623. doi:10.24963/kr.2020/61. [9] 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. [10] S. Demri, K. Quaas, First Steps Towards Taming Description Logics with Strings, in: S. Gaggl, M. V. Martinez, M. Ortiz (Eds.), Logics in Artificial Intelligence, Lecture Notes in Computer Science, Springer Nature Switzerland, Cham, 2023, pp. 322–337. doi:10.1007/978-3-031-43619-2_23. [11] F. Baader, J. Rydval, Description Logics with Concrete Domains and General Concept Inclusions Revisited, in: N. Peltier, V. Sofronie-Stokkermans (Eds.), Automated Reasoning, Lecture Notes in Computer Science, Springer International Publishing, Cham, 2020, pp. 413–431. doi:10.1007/ 978-3-030-51074-9_24. [12] S. Borgwardt, F. De Bortoli, P. Koopmann, The Precise Complexity of Reasoning in π’œβ„’π’ž with πœ”-Admissible Concrete Domains (Extended Version), 2024. arXiv:2405.19096. [13] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge University Press, 2017. doi:10.1017/9781139025355. [14] P. Koopmann, Signature-based abduction with fresh individuals and complex concepts for de- scription logics, in: Z. Zhou (Ed.), Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI, ijcai.org, 2021, pp. 1929–1935. doi:10.24963/IJCAI.2021/266. [15] F. Baader, F. De Bortoli, 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 ’24, ACM, New York, NY, USA, 2024, pp. 754–761. doi:10.1145/3605098.3635984.