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 afecting the complexity.
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 [
Unfortunately, dealing with feature paths in DLs is very challenging and often leads to undecidability [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 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 ifnitely 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].
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
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 equality relation = between two elements of D; D that defines the 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 if (1, . . . , ) ∈ C holds for all 1, . . . , ∈ (B) ∩ (C) and all -ary predicates over D, then B and C are satisfiable if 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 difers 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 Section 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 diferent, 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 [
Definition 2.
A set ⊆ ℳ
is a type w.r.t. if it satisfies the following properties: • if ⊑ ∈ and ∈ , then ∈ ; • if ⊤ ∈ ℳ, then ⊤ ∈ ; • if ¬ ∈ ℳ, then ∈ if ¬ ∈/ ; • if ⊓ ′ ∈ ℳ, then ⊓ ′ ∈ if ∈ 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 if there is (1, . . . , ) ∈ C for some variables 1, . . . , such that
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 difer 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) if 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); • for every ( 11 , . . . , ) ∈ Ct , we have (1,1 , . . . , , ) ∈ C; • for every ¬∃1, . . . , . ∈ root(t), there can be no (1, . . . , ) ∈ C with ⎪⎩ , if = and ∈ succt ();
if = and (, ) ∈ , or
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
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 elimination 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 return consistent return inconsistent 1: ℳ ← 2: T ←
Input: An ℒ(D) ontology = ∪
all subconcepts occurring in and their negations
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 types to define ∆ +1[, ] := {(, · (u, )) | ∈ succt()} to then obtain 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 ∆ +1 based on ∆ , and subsequently ∆ +1 := ∆ ∪
⋃︁ {︀ ∆ +1[, ] | (, ) ∈ ∆ and ∈ NR}︀ and set ∆ ℐ := ⋃︀ ∈N
∆ . The interpretation of individual, concept, and role names over ℐ is given by ℐ := (, ), ℐ := {︀ (, ) ∈ ∆ ℐ | end() = t and ∈ root(t)}︀ , ℐ := {︀ ((, ), (, )) | (, ) ∈ ∪
︀} ︀{ ((, ), (, ′)) | (, ) ∈ ∆ and (, ′) ∈ ∆ +1[, ] with ∈ N︀} .
Defining the interpretation of feature names in ℐ requires more work. Given (, ) ∈ ∆ ℐ with following claims can be found in [12]. 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 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 union of all systems C for ∈ N. Every finite system B ⊆ ∈ 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 , Cℐ is also a subsystem of C for some ℐ. Let Cℐ be the occurs in Cℐ , and leave it undefined otherwise.
Claim 2. If ∈ ℳ and (, ) ∈ ∆ ℐ with end() = t, then ∈ root(t) if (, ) ∈ ℐ .
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
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, ℐ := {︀ ℐ () | ∈ ∆ ℐ }︀ . we build the augmented type tℐ () = (0, . . . , , C) as follows.
First, we set 0 := ℐ () ∈ ℐ . Assuming that ∃. ∈ 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 ∈ ∆ ℐ , ℳ for = 1, . . . , ex, we select types ∈ ∆ ℐ , and thus of Tℐ . pick as the type of an arbitrary element in ∆ ℐ . 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 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(,) C that contains the constraint (︀ 11 , . . . , )︀ if (︀ 1ℐ (1 ), . . . , ℐ ( ) ︀) has not been selected this way, let off(,) be the type of an arbitrary individual in ∆ ℐ . Similarly, if ∃1 , . . . , . ∈/ 0 then we set off(,) be the type of an arbitrary individual in ∆ ℐ for = 1, . . . , ar.
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 ∈ 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 Claim 3. Every augmented type in Tℐ is locally realizable and patched in Tℐ . ∈ {0, . . . , }, we define the constraint system
C s.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 (1 1,1 , . . . ,
, ) ∈ C if (1ℐ (1,1 ), . . . , ℐ (, )) ∈ . and (ℐ , ℐ ) ∈ ℐ .
Finally, we define the set to consist of all role assertions (, ) for which , ∈ NI(), ∈ NR(), 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. following theorem (a detailed proof can be found in [12]).
We can show in a standard way that Algorithm 1 runs in exponential time w.r.t. and obtain the Theorem 8. Let D be an ExpTime--admissible concrete domain. Then, the consistency problem for ℒ(D) ontologies is ExpTime-complete.
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 diferent 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 sufices 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ℐ ), . . . , ℐ (ℐ )︀) ∈ if (1, . . . , ) ∈ , for all combinations of feature assertions (, ) in . By JD, this in particular implies that 1ℐ (1ℐ ) = 2ℐ (2ℐ ) if 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 ℐ′ () := ℎ( ℐ ()) if 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).
In this paper, we revisited the problem of reasoning in ℒ(D) with an -admissible concrete domain 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 requirement 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 diferent 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 ℒ.
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. 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. Safiotti (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 description 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.