On the Abstract Expressive Power of Description Logics with Concrete Domains

Abstract

Concrete domains have been introduced in Description Logic (DL) to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. The primary research goal in this context was to find restrictions on the concrete domain such that its integration into certain DLs preserves decidability or tractability. In this paper, we investigate the abstract expressive power of logics extended with concrete domains, namely which classes of first-order interpretations can be expressed using these logics. In the first part of the paper, we show that, under natural conditions on the concrete domain D (which also play a role for decidability), extensions of first-order logic ( FOL) or ℒ with D share important formal properties with FOL, such as the compactness and the Löwenheim-Skolem property. Nevertheless, their abstract expressive power need not be contained in that of FOL. In the second part of the paper, we investigate whether finitely bounded homogeneous structures, which preserve decidability if employed as concrete domains, can be used to express certain universal first-order sentences, which then could be added to DL knowledge bases without destroying decidability. We show that this requires rather strong conditions on said sentences or an extended scheme for integrating the concrete domain that leads to undecidability.

Keywords

• eol>Description Logics
• Concrete Domains
• Model Theory
• Expressive Power

1. Introduction

Most DLs [ 1 ] are decidable fragments of first-order logic ( FOL), i.e., their expressive power [ 2, 3 ] is below that of FOL, but there are also decidable DLs whose knowledge bases (KBs) cannot always be expressed by an FOL sentence [ 4 ]. A case in point are DLs with concrete domains [ 5, 6 ], at least at first sight. In such DLs we can refer to elements of the concrete domain and use predefined constraints over these elements when defining concepts. For example, assume that we want to model physical objects, collected in a concept (i.e., unary predicate) PO , which can be decomposed into their proper parts using a role (i.e., binary predicate) hpp for “has proper part.” If we want to take the weight of such objects into account, it makes sense to assign a number for its weight to every physical object using a feature (i.e., partial function) , and to state that this weight is positive and that proper parts are physical objects that have a smaller weight than the whole. Using the syntax employed in [ 6, 7 ] and in the present paper, these conditions can be expressed with the help of value restrictions and concrete domain restrictions w.r.t. an appropriate concrete domain by the following concept inclusion (CI): PO ⊑ ∀hpp. PO ⊓ ∃. (1 > 0) ⊓ ∀, hpp . >(1, 2). (1) Depending on what kind of decomposition into proper parts we have in mind, we can use the rational numbers or the integers as concrete domain. The former would be more appropriate for settings like cutting a cake, where a given piece can always be cut into even smaller parts, whereas the latter is more appropriate for settings where physical objects are composed of ifnitely many atomic parts that cannot be divided any further. Interestingly, as we will show in this paper, this decision also has an impact on the formal properties that the logic (in the example, the DL ℒ) extended with such a concrete domain satisfies. If we employ the integers, then for any element of PO there is a positive integer such that the length of all hpp-chains issuing from it are bounded by this number. Using this fact, it is easy to show that the logic at hand is not compact, i.e., there may be unsatisfiable infinite sets of sentences for which all ifnite subsets are satisfiable. In particular, this implies that the abstract expressive power of this logic, which considers only the abstract domain and the interpretation of concept and role names, but ignores the feature values, cannot be contained in FOL. For the rational numbers, the results obtained in this paper imply that the extension of ℒ or FOL with this concrete domain shares the compactness and the Löwenheim-Skolem property with FOL. The reason is that the rational numbers with > are homomorphism -compact [ 8, 7 ], which means that a countable set of constraints is solvable if all its finite subsets are solvable. We can, however, prove that the abstract expressive power of these logics is nevertheless not contained in FOL.

In the presence of CIs, integrating even rather simple concrete domains into the DL ℒ may cause undecidability [ 9, 8 ]. To overcome this problem, the notion of -admissible concrete domains was introduced in [ 6 ], and it was shown that integrating such a concrete domain into ℒ leaves reasoning decidable also in the presence of CIs. Since -admissibility requires a rather complex combination of conditions (including homomorphism -compactness), no new -admissible concrete domains were exhibited after the publication of [ 6 ], until [ 8, 7 ] related -admissibility to well-known notions from model theory. In particular, it was shown there that finitely bounded homogeneous structures yield -admissible concrete domains. Since such structures can be defined using universal first-order sentences, our question was whether the abstract part of a model of a KB can be forced to satisfy said sentences using appropriate CIs. Note that role inclusion axioms (RIAs) are universal first-order sentences, which preserve decidability if they satisfy a certain regularity condition [ 10, 11 ]. It is not clear whether regularity of a finite set of RIAs is decidable, though there are decidable suficient conditions for regularity [ 10, 11 ]. As proved in [ 8, 7 ], it is actually decidable whether a given universal first-order sentence induces a finitely bounded homogeneous structure or not. Our hope was that adding universal first-order sentences that induce finitely bounded homogeneous structures to a KB could be shown to preserve decidability using decidability of the corresponding DL with such structures as concrete domain. Unfortunately, it turns out that this reduction does not work in general. We considered two ways for overcoming this problem. One puts additional conditions on the universal firstorder sentences. Whereas then the reduction indeed works, the condition is so strict that decidability can also be shown using known results for conjunctive query answering w.r.t. ℒ ontologies [ 12 ]. Our second approach uses negated roles in concrete domain restrictions. In our example, we could then also describe the class of physical objects whose weight is not larger than the weight of any object that is not a proper part of it as ∀, ¬hpp . ≤ (1, 2). We can show, however, that such an extension may cause undecidability even for a concrete domain that is finitely bounded and homogeneous.

2. Logics with Concrete Domains

We define the notion of first-order logic with concrete domains, and introduce DLs with concrete domains as fragments. Then, we define the notion of abstract expressive power of a logic with concrete domains. But first, we recall some algebraic notions that are needed later on. Relational structures. A relational signature is a set of relation symbols, each with an associated natural number called its arity. A relational -structure A (or simply -structure or a structure) consists of a set , called its domain, together with relations ⊆ for each symbol ∈ of arity . The structure A is called finite if its domain is finite. A homomorphism between -structures A and B is a mapping ℎ : → such that ¯ ∈ implies ℎ(¯) ∈ for ¯ ∈ and ∈ a -ary relation. We write A → B if there is a homomorphism from A to B. We say that the homomorphism ℎ is strong if ¯ ∈ if ℎ(¯) ∈ holds. An embedding is an injective strong homomorphism between structures, while an isomorphism is a surjective embedding. An automorphism is an isomorphism from a structure to itself. If ⊆ and A embeds into B, we say that A is a (induced) substructure of B and B an extension of A. Concrete domains. From an algebraic point of view, a concrete domain is a -structure D for a relational signature , and a constraint system for D is a -structure A. This constraint system is satisfiable in D if A → D and unsatisfiable otherwise. We call a homomorphism ℎ : → a solution of A in D. For example, consider the structure Q := (Q, <) of rational numbers with the standard ordering relation. The structure A := ({1, 2}, {(1, 2), (2, 1)}) is a finite constraint system that is unsatisfiable in Q. As a formula, this can be written as 1 > 2 ∧ 2 > 1, and the fact that A ̸→ Q corresponds to the fact that one cannot assign elements of Q to the variables 1, 2 such that this formula becomes true in Q. First-order logic with concrete domains. Let D be a concrete domain over a relational signature , be a first-order signature, and ℱ be a countable set of feature symbols. The formulae of first-order logic with the concrete domain D, FOLℱ (D) (or simply FOL(D)), are obtained by extending the usual inductive definition for FOL with the following two base cases: • definedness predicates Def( )() with ∈ ℱ and a -term, and • concrete domain predicates (1, . . . , )(1, . . . , ) with ∈ , ∈ ℱ , -terms. The semantics of FOL(D) formulae is defined inductively, using a first-order interpretation ℐ = (∆ ℐ , · ℐ ) for extended with a set F of partial functions F : ∆ ℐ ⇀ for ∈ ℱ , and an assignment mapping variables to elements of ∆ ℐ . The semantics of terms, Boolean connectives and first-order quantifiers is defined as usual, where we denote the interpretation of a term by ℐ and as ℐ,. The new predicates are interpreted as follows: • (ℐ, F), |= Def( )() if F(ℐ,) is defined, and • (ℐ, F), |= (1, . . . , )(1, . . . , ) if (1F(1ℐ,), . . . , F (ℐ,)) ∈ . symbols (ℐ, F) |= , if (ℐ, F), |= for some (and thus all) assignments . Note that (1F(1ℐ,), . . . , F (ℐ,)) ∈ entails that F(ℐ,) must be defined for = 1, . . . , . The tuple (ℐ, F) is a model of the FOL(D) sentence (i.e., formula without free variables), in by adding these restrictions as concept constructors with ℒ(D). ¯= Description Logics with concrete domains. For an arbitrary DL ℒ, a given concrete domain D can be integrated into ℒ with the help of concrete domain restrictions. Concrete domain restrictions for D are concept constructors of the form ∃¯. (¯) or ∀¯. (¯) , with 1, . . . , a sequence of feature paths, a -ary predicate of D, and ¯= 1, . . . , a -tuple of variables. In the context of this paper, a feature path is either a feature name or an expression with a feature name and a role name. We denote the DL obtained from ℒ concrete domain restrictions is then defined as follows:

To define the semantics of ℒ(D), we assume that concepts of ℒ can be translated into FOL formulae with one free variable using a translation function . We extend this translation function to map concepts of ℒ(D) to formulae of FOL(D) by providing the translation of concrete domain restrictions. Taking ¯, ¯ as defined above, let ⊆ { 1, . . . , } be such that = if ∈ and = otherwise. We define ¯:= 1, . . . , by setting = if ∈ and = otherwise, and ¯ as the sequence of variables with ∈ . The translation of (∃¯. (¯)) := (∀¯. (¯)) := ∀¯.

︁( ∃¯. (︀ ⋀︀ ∈ (, ) ∧ (1, . . . , )(¯) )︀ , ⋀︀ ∈ (, ) ∧ ⋀︀ =1 Def()()

→ (1, . . . , )(¯) . ︁) ︁) (2) The semantics of TBoxes and ABoxes of the DL ℒ(D) is then defined in the usual way by translation into FOL(D) sentences. It is easy to see that the semantics of concrete domain restrictions given by the translation in (2) coincides with the direct model-theoretic semantics in [ 6, 7 ]. In [ 6 ], extensions of the predicates of a concrete domain D by disjunctions of its base predicates are allowed to be used in concrete domain restrictions, whereas in [ 7 ] even predicates ifrst-order definable from the base predicates are considered. These extensions can clearly also be translated into FOL(D). We denote them as ℒ∨+ (D) and ℒfo(D), respectively. Abstract expressive power. If we want to compare the expressive power of (a fragment of) FOL with that of (a fragment of) FOL(D), we have the problem that the semantic structures they are based on difer in that, for the latter, one additionally has a collection of partial functions into the concrete domain. To overcome this diference, we say that the first-order interpretation to the FOL(D) sentence if the abstract models of are exactly the models of . an abstract model of the FOL(D) sentence , in symbols ℐ |=D , if there is an interpretation of the feature symbols F such that (ℐ, F) |= . The FOL sentence is called abstractly equivalent ℐ is Example 1. Consider the concrete domain N := (N, even, odd, =) where even, odd are unary relations and = is a binary relation, with the standard meaning. We can always force the interpretation of a feature name to be a total function using the inclusion ⊤ ⊑ ∃, .=(1, 2). This implies that := { ⊑ ∀.even(), ⊑ ∀.odd(), ⊤ ⊑ ∃, .=(1, 2)} is an ℒ(N) TBox abstractly equivalent to ≡ ¬ .

The abstract expressive power of (a fragment of) FOL(D) is determined by which classes of abstract models can be defined by its sentences. Given a fragment of FOL(D) (e.g., ℒ(D)), we say that its abstract expressive power is contained in FOL if every sentence of this fragment is abstractly equivalent to an FOL sentence.

Example 2. In the introduction we have given an example showing that, for a concrete domain D over the integers with predicates > and > 0, the abstract expressive power of ℒ(D) is not contained in FOL. The argument we have used there is based on the fact that FOL is compact, but ℒ(D) is not. In fact, the CI (1) enforces that, for any element of PO, there is a positive integer such that the length of all hpp-chains issuing from it are bounded by this number. Assume that is an FOL sentence that is abstractly equivalent to this CI. Clearly we can write, for all ≥ 1, an FOL sentence that says that the constant is an element of PO and the starting point of an hpp-chain of length . Then any finite subset of { } ∪ { | ≥ 1} is satisfiable, but the whole set cannot be satisfiable since the CI (1) enforces a finite bound on the length of chains issuing from . Since FOL is compact, this shows that cannot be a first-order sentence.

However, even if ℒ(D) is compact for a given concrete domain D, its abstract expressive power need not be contained in FOL.

Example 3. Consider the concrete domain Q := (Q, >, =, <). The results shown in the next section imply that the logic FOL(Q) is compact, and thus also its fragment ℒ(Q). Nevertheless, the abstract expressive power of ℒ(Q) is not contained in FOL. To see this, consider the CI ⊤ ⊑ ∃, .=(1, 2) ⊓ ∀, .>(1, 2) and assume that there is an FOL formula that is equivalent to it. Then (Q, >), where > is the interpretation of , is an abstract model of the CI, and thus of . In fact, one can use the identity function to interpret the feature . It is wellknown that (Q, >) and (R, >) are elementary equivalent, i.e., satisfy the same FOL formulae. Consequently, (R, >) is a model of , and thus an abstract model of the CI. This means that there is an interpretation F of such that ((R, >), F) is a model of the above CI. As seen in Example 1, the conjunct ∃, .=(1, 2) forces F to be total. Assume that , are distinct real numbers, and (w.l.o.g) that > . Then the restriction ∀, .>(1, 2) implies F( ) > F( ), and thus F( ) ̸= F( ). This shows that F is injective. However, since R is uncountable and Q is countable, there cannot be an injective function from R to Q. 3. First-order Properties of Logics with Concrete Domains First-order logic satisfies a number of interesting formal properties, usually shown in any introductory textbook in logic [ 13, 14 ]: (Downward) Löwenheim-Skolem: If a sentence is satisfiable, then it has a model whose domain is at most countable (Upward) Löwenheim-Skolem: If a sentence has a model with an infinite domain, then it has a model with an uncountable domain (Countable) Compactness: If Φ is a countable set of sentences and every finite subset of Φ is satisfiable, then Φ is satisfiable.

We will show that, under natural conditions on the concrete domain D, FOL(D) shares most and ℒ(D) shares all of these properties with FOL. The first condition states that constraint solving in D is compact in the sense that a countable constraint system for D is satisfiable if every of its finite subsets is satisfiable. In the algebraic language introduced in the previous section, this condition is called homomorphism -compactness. Note that this is one of the conditions required for -admissibility of a concrete domain [ 6 ].

Definition 1. The age of a -structure B, denoted with Age(B), is the set of all finite -structures A such that A embeds into B. A concrete domain D is homomorphism -compact if, for every countable -structure B, B is satisfiable in D if every A ∈ Age(B) is satisfiable in D.

The second condition is that the concrete domains D is closed under negation, i.e. for every predicate symbol of D there is a predicate symbol of D such that ¯ ∈ if ¯ ∈/ . This condition appears in the definition of admissibility for concrete domains [ 5 ], and is needed since our logics can express negation of concrete domain predicates. We assume in this section that the concrete domain D is homomorphism -compact and closed under negation. The main tool for showing our results is a satisfiability-preserving translation of sets of FOL(D) sentences into sets of FOL sentences.

First-order translation. Let Φ be a (possibly infinite) set of FOL(D) sentences. We translate Φ into a set of FOL sentences Φ FOL by replacing every atom of the form (1, . . . , )(1, . . . , ) occurring in Φ with 1,..., (1, . . . , ), where for every -ary concrete domain predicate and features 1, . . . , we assume that 1,..., is a new -ary predicate symbol in the ifrst-order signature. Similarly, every atom of the form Def( )() is replaced with Def () where Def is a new predicate symbol for every feature . Every set Γ of atoms of the form 1,..., (1, . . . , ) induces a constraint system BΓ with relations

Γ := {(11 , . . . , ) | 1,..., (1, . . . , ) ∈ Γ } and domain Γ consisting of all elements occurring in some relation.

To capture the semantics of the concrete domain predicates and the definedness predicate, we additionally consider the set of FOL sentences Ψ D consisting of: • for each of the new predicate symbols 1,..., the sentences

∀1, . . . , . 1,..., (1, . . . , ) ∀1, . . . , .¬ 1,..., (1, . . . , ) → →

Def1 (1) ∧ . . . ∧ Def (),

1,..., (1, . . . , ) ∨ ⋁︁ ¬ Def (), =1 • for every finite set Γ of atoms of the form 1,..., (1, . . . , ) the sentence ∀⃗. ⋀︀ Γ → ⊥ if BΓ is unsatisfiable in D, where ⃗ collects all the variables occurring in Γ . Theorem 1. Let D be a homomorphism -compact concrete domain that is closed under negation. The set of FOL(D) formulae Φ is satisfiable in FOL(D) if Φ FOL ∪ Ψ D is satisfiable in FOL. Proof sketch. First, assume that Φ FOL ∪Ψ D is satisfiable. Since this is a countable set of first-order formulae, the downward Löwenheim-Skolem property of FOL implies that there is an at most countable model I of Φ FOL ∪ Ψ D. We show that we can extend I with an interpretation F of the features such that (I, F) is a model of Φ . To this purpose, consider the set Γ I consisting of all expressions 1,..., (1, . . . , ) that are satisfied in I, where 1, . . . , ranges over all elements of I and 1, . . . , over all feature names. Let BI be the constraint system induced by Γ I. Due to our construction of Ψ D and the fact that I is a model of this set, we know that each of the finite substructures of BI is satisfiable in D. Since BI has countable domain and signature, homomorphism -compactness implies that there exists a solution ℎ of BI in D. For all feature names and elements ∈ for which ∈ I, we define F() := ℎ(). Otherwise, we choose an arbitrary value for F() if Def () is true in I, and leave F() undefined if false. The fact that, together with this interpretation of the features F, the FOL interpretation I is indeed a model of Φ , is an immediate consequence of the following two claims (we refer to the appendix of [15] for a proof): 1. Def () is true in I if Def( )() is true in (I, F); 2. 1,..., (1, . . . , ) is true in I if (1, . . . , )(1, . . . , ) is true in (I, F).

Second, assume that Φ is satisfiable in FOL(D) by the interpretation I of the FOL part and the interpretation F of the features. We extend I to an interpretation J that also takes the new predicates Def and 1,..., into account: • belongs to Def in J if F() is defined, • (1, . . . , ) belongs to 1,..., in J if (1F(1), . . . , F ()) holds in D. Since (I, F) makes Φ true, it is easy to see that J is a model of Φ FOL. In addition, it is a model of Ψ D due to the semantics of concrete domain restriction in FOL(D) and the fact that is the complement of in D.

Thanks to this theorem, we can transfer some properties of FOL to FOL(D). Corollary 1. If D is a homomorphism -compact concrete domain that is closed under negation, then FOL(D) is countably compact and satisfies the downward Löwenheim-Skolem property. Homomorphism -compactness is also a necessary condition for countable compactness. In general, FOL(D) need not satisfy the upward Löwenheim-Skolem property.

Proof sketch. Compactness follows from Theorem 1. In fact, if Φ is unsatisfiable, then this theorem and compactness of FOL yield a finite subset Ψ of Φ FOL ∪ Ψ D that is unsatisfiable. Then translating Ψ ∩ Φ FOL back to FOL(D) yields an unsatisfiable finite subset of Φ . The downward Löwenheim-Skolem property follows from the construction of the abstract model I in the if-direction of Theorem 1, which is at most countable.

Assume that the -structure B is a counterexample to the homomorphism -compactness of D. Then Γ B := {∀.( (1, . . . , )(, . . . , )) | ∈ and (1, . . . , ) ∈ } is a set of FOL(D) sentences that is a counterexample to countable compactness of FOL(D).

Finally, consider the concrete domain Q= := (Q, =, ̸=), which is closed under negation and easily seen to be homomorphism -compact. The FOL(Q=) sentence

up := ∀, . Def( )() ∧ ( ̸= → ̸=(, )(, )) states that is an injective function from the domain of an abstract model of up into Q. Thus, no abstract model of up can have an uncountable domain, as Q is is countable.

For ℒ with a concrete domain, we can strengthen the result above and obtain the following. Corollary 2. Let D be a homomorphism -compact concrete domain that is closed under negation, and ℒ ∈ {ℒ(D), ℒ∨+ (D), ℒfo(D)}. Then ℒ is countably compact and satisfies the upward and the downward Löwenheim-Skolem property. Homomorphism -compactness is also a necessary condition for countable compactness.

Proof sketch. Compactness and the downward Löwenheim-Skolem property are an immediate consequence of the fact that ℒ can be expressed in FOL(D). Regarding necessity of homomorphism -compactness, it is easy to see that a counterexample B to this property can also be turned into a counterexample to countable compactness of ℒ, similar to our construction for FOL(D). The upward Löwenheim-Skolem is an immediate consequence of the fact that, like ℒ [ 1 ], its extension ℒ is closed under disjoint unions (proof in the appendix of [15]).

4. Bounding Models through Concrete Domains

In [ 7 ], it was shown that finitely bounded structures that are also homogeneous yield admissible concrete domains, and thus preserve decidability if integrated into the DL ℒ. Finitely bounded structures can be defined using finitely many forbidden finite substructures, which are usually called bounds. Here, we employ an alternative definition that uses universal FOL sentences: a relational structure A with a finite signature is finitely bounded if Age(A) is the class of all finite models of some universal -sentence Φ (see Lemma 3 in [ 7 ]). We say in this case that Age(A) is defined by Φ . A structure A is homogeneous if every isomorphism between ifnite substructures of A extends to an automorphism of A. As pointed out in [ 7 ], countable relational structures with a finite signature that are homogeneous are also homomorphism -compact. In addition, given a universal FOL sentence Φ over at most binary relation symbols, it is decidable in Π 2 if Φ defines the age of a homogeneous structure A (Theorem 15 in [ 7 ]). The question is now whether, in this setting, one can use an ℒ(A) TBox ℎ to express that the concept and role names of a given ℒ TBox must satisfy Φ . Note that, as just pointed out, for a given universal sentence Φ it is decidable whether it induces a finitely bounded homogeneous structure A). If this is the case, then reasoning w.r.t. ∪ ℎ, and thus w.r.t. and Φ , is decidable. To be more precise, given an ℒ TBox and a universal first-order sentence Φ over its concept and role names := ∪ , we first check, using the decision procedure in [ 7 ], whether Φ defines the age of a nfiitely bounded homogeneous structure. If this is the case, then let DΦ be this structure. The results in [ 7 ] imply that reasoning in ℒ(DΦ) is decidable. Next, we define the ℒ(DΦ) TBox

ℎ := {⊤ ⊑ ∃, .=(, )}∪{ ⊑ ∀.() | ∈ }∪{⊤ ⊑ ∀, .(, ) | ∈ } (3) which encodes the existence of a homomorphism from its abstract models to DΦ. Lemma 1. The interpretation ℐ is an abstract model of ℎ if ℐ → DΦ. This implies that every model of Φ is an abstract model of ℎ.

Proof. The first part of the lemma is an easy consequence of the definition of ℎ. To prove the second part, assume that ℐ is a model of Φ . By preservation of universal sentences under taking substructures [16], we obtain that A |= Φ for every A ∈ Age(ℐ), which shows that Age(ℐ) ⊆ Age(DΦ) since Φ defines Age(DΦ). The elements of Age(DΦ) embed into DΦ by definition, and embeddings are homomorphisms. This shows that all the elements of Age(ℐ) are satisfiable in DΦ. Since DΦ is homomorphism -compact, we deduce that ℐ is satisfiable in DΦ. The first part of the lemma thus yields that ℐ is an abstract model of ℎ.

Unfortunately, under the assumptions made in this lemma, we cannot conclude that every abstract model of ℎ is a model of Φ . In fact, assume that ℐ is a model of ℎ that is not a model of Φ , i.e., ℐ |= ¬Φ . We could lead this assumption to a contradiction if we were able to show that this implies that DΦ is a model of ¬Φ . However, all we know about the relationship between ℐ and DΦ is that ℐ → D. Since existential sentences (like ¬Φ ) are in general not preserved under homomorphisms, we cannot conclude from ℐ |= ¬Φ that DΦ |= ¬Φ . Example 7 in the appendix of [15] shows an actual counterexample. We look at two ways to overcome this problem: imposing further restrictions on Φ or adding further GCIs to ℎ. Imposing further restrictions on Φ . We have seen above that the source of our problem is that general existential sentences need not be preserved under homomorphisms. However, it is well-known that existential positive sentences are [16]. Let us write nnf() to denote the negation normal form of a sentence . To obtain the desired result, it is enough to assume that nnf(¬Φ) is existential positive.

Theorem 2. Let DΦ be a finitely bounded homogeneous structure whose age is defined by the universal sentence Φ . If nnf(¬Φ) is existential positive, then ℎ and Φ are abstractly equivalent. Proof. Assume that ℐ is an abstract model of ℎ. By Lemma 1, there is a homomorphism from ℐ to DΦ. Let Ψ := nnf(¬Φ) . If ℐ ̸|= Φ , then ℐ |= ¬Φ and in particular ℐ |= Ψ . Since Ψ is existential positive, this implies DΦ |= Ψ . Since Ψ is existential, this in turn implies that there is a finite substructure A of DΦ such that A |= Ψ , namely the substructure induced by the elements with which the existentially quantified variables of Ψ are instantiated. Since A belongs to Age(DΦ), this yields a contradiction, which shows that ℐ |= Φ . The other direction has been shown in the proof of Lemma 1.

Under the assumptions made in this theorem, reasoning in ℒ(DΦ) is decidable. Thus, the abstract equivalence of Φ and the ℒ(DΦ) TBox ℎ implies that we can add the universal formula Φ to any ℒ KB without losing decidability. However, the assumption that nnf(¬Φ) is existential positive is so strong that decidability holds even if Φ does not define the age of a ifnitely bounded homogeneous structure.

Proposition 1. Let Φ be a universal first-order sentence over ∪ s.t. nnf(¬Φ) is existential positive. Then, checking if a given ℒ KB ( , ) has a model that satisfies Φ is decidable. Proof. To decide whether ( , ) has a model that also satisfies Φ , it is enough to check whether ( , ) entails ¬Φ . Since ¬Φ is existential positive, it is equivalent to a union of Boolean conjunctive queries. Decidability of entailment of such a union by an ℒ KB is known to be ExpTime-complete [ 12 ].

Extending the TBox. The TBox ℎ encodes the existence of a homomorphism from its abstract models to the concrete domain DΦ. We have seen above that, without further restrictions on Φ , this does not ensure that the abstract models of ℎ are also models of Φ . The following proposition shows that it would be suficient to encode the existence of a strong homomorphism. Proposition 2. If an equality-free first-order sentence Ψ is equivalent to an existential sentence, then it is preserved under strong homomorphisms.

Proof. Assume w.l.o.g. that Ψ is in negation normal form, and let the -structure A be a model of Ψ with a strong homomorphism ℎ : A → B. Let ′ := ∪ { | ∈ }. We expand A into A′ by setting ′ := ∖ for every -ary ∈ ; likewise, we expand B into B′. Then, ℎ : A′ → B′ is a homomorphism. If we replace every occurrence of ¬ in Ψ with , then A′ is a model of the resulting existential positive sentence Ψ ′. Using homomorphism preservation of existential positive sentences, we obtain that B′ |= Ψ ′, which shows B |= Ψ .

To encode the existence of a strong homomorphism between abstract models and the concrete domain, we need to extend the interface between the abstract and the concrete domain, which are the concrete domain restrictions ∃¯. (¯) and ∀¯. (¯) . As introduced in Section 2, the feature paths in ¯ are of the form or for feature names and role names . We extend this interface by allowing the use of negated roles ¬ in addition to role names in such paths. The semantics of the resulting concrete domain restrictions is defined analogously to the translation (2), where ¬(, ) is used instead of (, ) if = ¬. With this extension, we are now able to extend ℎ to encode the existence of a strong homomorphism by adding ¬ ⊑ ∀.¬() for ∈ and ⊤ ⊑ ∀, ¬.¬(, ) for ∈ . We denote with ℎ the resulting TBox. Theorem 3. Let DΦ be a finitely bounded homogeneous structure whose age is defined by the universal sentence Φ . Then ℎ and Φ are abstractly equivalent.

Proof. It is again easy to see that ℐ is an abstract model of ℎ if there exists a strong homomorphism from ℐ to DΦ. Now, assume that ℐ |=DΦ ℎ, and let ℎ : ℐ → DΦ be the corresponding strong homomorphism. If ℐ ̸|= Φ , then ℐ |= ¬Φ . Since nnf(¬Φ) is an existential formula, Proposition 2 yields DΦ |= ¬Φ . We can now argue as in the proof of Theorem 2 that this yields a contradiction. This shows that ℐ |= Φ must hold. The other direction can been shown similarly to the proof of Lemma 1, using the fact that embeddings are strong homomorphisms, extending the signature by new predicates for negated predicates as in the proof of Proposition 2, and using the fact the corresponding expanded structure D˜ Φ is again finitely bounded and homogeneous (see the proof of Proposition 7 of [ 7 ]).

Unfortunately, we cannot use this theorem to show that one can add such a formula Φ to an ℒ KB without destroying decidability. The reason is that allowing for negated roles in feature paths of concrete domain restrictions may cause undecidability, even if the employed concrete domain is given as a finitely bounded homogeneous structure.

Theorem 4. There is a finitely bounded homogeneous structure D such that the extension of ℒ∨+ (D) with negated roles in feature paths is undecidable.

The structure used in the proof of this theorem (see the appendix of [15] for details) is obtained as the full product of Q := (Q, <, =, >) with itself. Since Q is a finitely bounded homogeneous structure, and such structures are closed under full product [ 7 ], this product Q2 is also a finitely bounded homogeneous structure. In Q2 one has domain Q2 and copies <, =, > for = 1, 2 of the relations of Q, which in their dimension act like the corresponding relation in Q. In the other dimension they do not impose any constraint. The idea is now that one can employ this grid-like structure on the side of the concrete domain to express a grid in the abstract domain, which can then be used to reduce the tiling problem to consistency of a ℒ∨+ (Q2) TBox.

5. Conclusion

The starting point of this work were two conjectures regarding DLs with concrete domains, which turned out to be wrong. However, our attempts to prove these conjectures considerably increased our understanding of such DLs and produced results that we think are interesting in their own right. Regarding the first conjecture, readers that know Lindström’s theorem [ 13, 17 ] may have wondered why it does not apply here. In fact, we have shown that FOL with a homomorphism -compact concrete domain is compact and satisfies the downward LöwenheimSkolem property. Lindström’s theorem says that a logical system extending FOL that satisfies these two properties is equivalent to FOL. This is the background for our original conjecture that the abstract expressive power of FOL extended with a homomorphism -compact concrete domain D is contained in FOL. So why does Lindström’s theorem not apply here? The reason is that, w.r.t. abstract expressive power, which forgets about the interpretation of features, FOL(D) is not a logical system in the sense of Lindström since it is not closed under conjunction. What still remains are our results that the extension of FOL with a homomorphism -compact concrete domain closed under negation satisfies compactness and downward Löwenheim-Skolem, and the corresponding extension of ℒ further satisfies upward Löwenheim-Skolem. Nevertheless, these logics need not be contained in FOL w.r.t. abstract expressive power.

Our second conjecture was motivated by the observation that (the age of) finitely bounded homogeneous structures, which yield -admissible concrete domains, are defined by universal ifrst-order formulae. The conjecture was that we could use this fact to show that certain universal first-order formulae can be added to ℒ KBs without destroying decidability. An advantage of this result, compared to results for regular RIAs, would have been that the class of universal first-order formulae that induce finitely bounded homogeneous structures in this way is decidable. Unfortunately, it has turned out that this conjecture is not correct. Our attempts to remedy this problem resulted either in a setting where decidability can be shown by other means or where the obtained DL with concrete domains is undecidable. We think that this undecidability result is also interesting in its own right.

Acknowledgments

This work was partially supported by the DFG TRR 248 (CPEC, grant 389792660). puter Science, 2. ed ed., Springer Science+Business Media, New York, 1996. doi:10.1007/ 978-1-4612-2360-3. [15] F. Baader, F. De Bortoli, On the Abstract Expressive Power of Description Logics with Concrete Domains (Extended Version), LTCS-Report 23-02, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden, Germany, 2023. https://tu-dresden.de/inf/lat/reports#BaBo-LTCS-23-02. [16] B. Rossman, Homomorphism preservation theorems, Journal of the ACM 55 (2008) 1–53.

doi:10.1145/1379759.1379763. [17] J. Väänänen, Lindström’s Theorem, in: J.-Y. Béziau (Ed.), Universal Logic: An Anthology, Springer Basel, Basel, 2012, pp. 231–235. doi:10.1007/978-3-0346-0145-0\_19.

References

[1] F. Baader , I. Horrocks, C. Lutz , U. Sattler , An Introduction to Description Logic, Cambridge University Press, 2017 . doi: 10 .1017/9781139025355.

[2] F. Baader , A formal definition for the expressive power of terminological knowledge representation languages , J. of Logic and Computation 6 ( 1996 ) 33 - 54 . doi: 10 .1093/ logcom/6.1.33.

[3] N. Kurtonina , M. de Rijke, Expressiveness of concept expressions in first-order description logics , Artificial Intelligence 107 ( 1999 ) 303 - 333 . doi: 10 .1016/S0004- 3702 ( 98 ) 00109 - X .

[4] 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.), Proc. of the 12th Int. Symposium on Frontiers of Combining Systems (FroCoS'19) , volume 11715 of Lecture Notes in Computer Science, Springer-Verlag, 2019 , pp. 203 - 219 . doi: 10 .1007/ 978-3- 030 -29007-8\_ 12 .

[5] 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.

[6] 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.

[7] 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.

[8] 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 .

[9] C. Lutz , NEXP TIME-complete description logics with concrete domains, ACM Transactions on Computational Logic (TOCL) 5 ( 2004 ) 669 - 705 . doi: 10 .1145/1024922. 1024925.

[10] I. Horrocks , U. Sattler, Decidability of ℋℐ with complex role inclusion axioms , Artificial Intelligence 160 ( 2004 ) 79 - 104 . doi: 10 .1016/j.artint. 2004 . 06 .002.

[11] Y. Kazakov , ℛℐ and ℛℐ are harder than ℋℐ , in: G. Brewka, J. Lang (Eds.), Proc. of the 11th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2008 ), AAAI Press, 2008 , pp. 274 - 284 .

[12] C. Lutz , The Complexity of Conjunctive Query Answering in Expressive Description Logics , in: A. Armando , P. Baumgartner , G. Dowek (Eds.), Automated Reasoning , volume 5195 , Springer Berlin Heidelberg, Berlin, Heidelberg, 2008 , pp. 179 - 193 . doi: 10 .1007/ 978-3- 540 -71070-7\_ 16 .

[13] H.-D. Ebbinghaus , J. Flum , W. Thomas, Mathematical Logic, Undergraduate Texts in Mathematics, second ed., Springer, New York, NY, 1994 . doi: 10 .1007/978-1- 4757 -2355-7.

[14] M. Fitting , First-Order Logic and Automated Theorem Proving, Graduate Texts in Com-