Description Logic TBoxes: Model-Theoretic Characterizations and Rewritability

1 Introduction

Since the emergence of description logics (DLs) in the 1970s and 80s, research in the area has been driven by the fundamental trade-off between expressive power and computational complexity [Baader et al., 2003]. Over the years, the idea of what complexity is 'acceptable' has varied tremendously, from insisting on tractability in the 1980s gradually up to NEXPTIME- or even 2NEXPTIME-hard DLs in the 2000s, soon intermixed with a revival of DLs for which reasoning is tractable or even in AC0 (in a database context). Nowadays, it is widely accepted that there is no universal definition of acceptable computational complexity, but that a variety of DLs is needed to cater for the needs of different applications. For example, this is reflected in the recent OWL 2 standard by the W3C, which comprises one very expressive (and 2NEXPTIME-complete) DL and three tractable 'profiles' to be used in applications where the full expressive power is not needed and efficient reasoning is crucial.

While DLs have greatly benefited from this development, becoming much more varied and usable, there are also new challenges that arise: how to choose a DL for a given application? What to do when you have an ontology formulated in a DL L, but would prefer to use a different DL L′ in your application? How do the various DLs interrelate? The first aim of this paper is to lay ground for the study of these and similar questions by providing exact model-theoretic characterizations of the expressive power of TBoxes formulated in the most important DLs, including expressive ones such as ALC and ALCQIO (the core of the expressive DL formalized as OWL 2) and lightweight ones such as EL and DL-Lite (the cores of two of the OWL 2 profiles). We characterize the expressive power of DL TBoxes relative to first-order logic (FO) as a reference point, which (indirectly) also yields a characterization of the expressive power of a DL relative to other DLs. The second aim of this paper is to exemplify the use of the obtained characterizations by developing algorithms for the novel decision problem L1-to-L2-TBox rewritability: given an L1-TBox T , decide whether there is an L2-TBox that is equivalent to T . Note the connection to TBox approximation, studied e.g. in [Ren et al., 2010; Botoeva et al., 2010; Tserendorj et al., 2008]: when L1 is computationally complex and the goal is to approximate T in a less expressive DL L2, the optimal result is of course an equivalent L2-TBox T ′ , i.e., when T can be rewritten into L2 without any loss of information.

We prepare the study of TBox expressive power with a characterization of the expressive power of DL concepts in Section 3. These are in the spirit of the well-known van Benthem Theorem [Goranko and Otto, 2007], giving an exact condition for when an FO-formula with one free variable is equivalent to a DL concept. We use different versions of bisimulation for ALC and its extensions, and simulations and direct products for EL and DL-Lite. There is related work by de Rijke and Kurtonina [Kurtonina and de Rijke, 1999], which, however, does not cover those DLs that are considered central today. We then move on to our main topics, characterizing the expressive power of DL TBoxes and studying TBox rewritability in Sections 4 and 5. To characterize when a TBox is equivalent to an FO sentence, we use 'global' and symmetric versions of the model-theoretic constructions in Section 3, enriched with various versions of (disjoint and non-disjoint) unions and direct products. These results are loosely related to work by Borgida [Borgida, 1996], who focusses on DLs with complex role constructors, and by Baader [Baader, 1996], who uses a more liberal definition of expressive power. We use our characterizations to establish decidability of TBox rewritability for the ALCI-to-ALC and ALC-to-EL cases. The algorithms are highly non-trivial and a more detailed study of TBox rewritability has to remain as future work.

Most proofs in this paper are deferred to the (appendix of the) long version, which is available as arXiv:1104.2844 [cs.LO].

2 Preliminaries

In DLs, concepts are defined inductively based on a set of constructors, starting with a set NC of concept names, a set NR of role names, and a set NI of individual names (all countably infinite). The concepts of the expressive DL ALCQIO are formed using the constructors shown in Figure 1.

In Figure 1 and in general, we use rI (d) to denote the set of all r-successors of d in I, #S for the cardinality of a set S, a and b to denote individual names, r and s to denote roles (i.e., role names and inverses thereof), A, B to denote concept names, and C,D to denote (possibly compound) concepts. As usual, we use ⊤ as abbreviation for A⊔¬A, ⊥ for ¬⊤, → and ↔ for the usual Boolean abbreviations, ∃r.C (existential restriction) for (⩾ 1 r C), and ∀r.C (universal restriction) for (⩽ 0 r ¬C).

Throughout the paper, we consider the expressive DL ALCQIO, which can be viewed as a core of the OWL 2 recommendation, and several relevant fragments; a basic such fragment underlying the OWL 2 EL profile of OWL 2 is the lightweight DL EL, which allows only for ⊤, ⊥, conjunction, and existential restrictions. By adding negation, one obtains the basic Boolean-closed DL ALC. Additional constructors are indicated by concatenation of a corresponding letter: Q stands for number restrictions, I for inverse roles, and O for nominals. This explains the name ALCQIO and allows us to refer to fragments such as ALCI and ALCQ. From the DL-Lite family of lightweight DLs [Calvanese et al., 2005; Artale et al., 2009], which underlies the OWL 2 QL profile of OWL 2, we consider DL-Litehorn whose concepts are conjunctions of basic concepts of the form A, ∃r.⊤, ⊥, or ⊤, where A ∈ NC and r is a role name or its inverse. We will also consider the DL-Litecore variant, but defer a detailed definition to Section 4. We use DL to denote the set of DLs just introduced, and ExpDL to denote the set of expressive DLs, i.e., ALC and its extensions introduced above.

The semantics of DLs is defined in terms of an interpretation I = (ΔI , ·I ), where ΔI is a non-empty set and ·I maps each concept name A ∈ NC to a subset AI of ΔI , each role name r ∈ NR to a binary relation rI on ΔI , and each individual name a ∈ NI to an aI ∈ ΔI . The extension of ·I to inverse roles and arbitrary concepts is inductively defined as shown in the third column of Figure 1.

For L ∈ DL, an L-TBox is a finite set of concept inclusions (CIs) C ⊑ D, where C and D are L concepts. An interpretation I satisfies a CI C ⊑ D if CI ⊆ DI and is a model of a TBox T if it satisfies all inclusions in T .

Concepts and TBoxes formulated in any L ∈ DL can be regarded as formulas in first-order logic (FO) with equality using unary predicates from NC, binary predicates from NR, and constants from NI. More precisely, for every concept C there is an FO-formula C ♯ (x) such that I |= C♯ [d] iff d ∈ C I , for all interpretations I and d ∈ ΔI [Baader et al., 2003]. For every TBox T , the FO sentence

is logically equivalent to T . We will often not explicitly distinguish between DL-concepts and TBoxes and their translation into FO. For example, we write T ≡ ϕ for a TBox T and an FO-sentence ϕ whenever T ♯ is equivalent to ϕ.

3 Characterizing Concepts

We characterize DL-concepts relative to FO-formulas with one free variable, mainly to provide a foundation for subsequent characterizations on the TBox level. We use the notion of an object (I, d), which consists of an interpretation I and a d ∈ ΔI and, intuitively, represents an object from the real world. Two objects (I1, d1) and (I2, d2) are L-equivalent, written (I1, d1) ≡L (I2, d2), if d1 ∈ C I1 ⇔d2 ∈ C I2 for all L-concepts C. Our first aim is to provide, for each L ∈ DL, a relation ∼L on objects such that ≡L ⊇ ∼L and the converse holds for a large class of interpretations. To ease notation, we use only d to denote the object (I, d) when I is understood.

We start by introducing the classical notion of a bisimulation, which corresponds to ≡ALC in the described sense. Two objects (I1, d1) and (I2, d2) are bisimilar, in symbols (I1, d1) ∼ALC (I2, d2), if there exists a relation S ⊆ ΔI1 × ΔI2 such that the conditions [Atom] (for A ∈ NC), [Forth] and [Back] from Figure 2 hold, where succIr (d) = {d′ ∈ ΔI | (d, d′ ) ∈ rI } and 'dual' refers to swapping the rˆoles of I1, d1, d′1 and I2, d2, d′2 ; we call such an S a bisimulation between (I1, d1) and (I2, d2). To address ALCQ, we extend this to counting bisimilarity (cf. [Janin and Lenzi, 2004]), in symbols ∼ALCQ, and defined as bisimilarity, but with [Forth] and [Back] replaced by [QForth] and [QBack] from Figure 2. Given ∼L, the relation ∼LO for the extension LO of L with nominals is defined by additionally requiring S to satisfy [Atom] for all concepts A = {a} with a ∈ NI. Similarly, ∼LI for the extension LI of L with inverse roles demands that in all conditions of ∼L, r additionally ranges over inverse roles.

Example 1. In Figure 3 (L), d1 ∼ALC d2 and a bisimulation is indicated by dashed arrows. In contrast, d1 ̸∼L d2 for L ∈ {ALCQ,ALCO,ALCI}. It is instructive to construct L-concepts C that show d1 ̸≡L d2.

We have provided a relation ∼L for each L ∈ ExpDL. For lightweight DLs with their restricted use of negation, it will be useful to consider non-symmetric relations between objects. A relation S ⊆ ΔI1 ×ΔI2 is an EL-simulation from I1 to I2 if it satisfies [AtomR] (for A ∈ NC) and [Forth] from Figure 2. S is a DL-Litehorn-simulation from I1 to I2 if it satisfies [AtomR] (for A ∈ NC) and [FSucc]. Let L ∈ {EL,DL-Litehorn}. Then (I1, d1) is L-simulated by (I2, d2), in symbols d1 ≤L d2, if there exists an L-simulation S with (d1, d2) ∈ S. The relation ∼L that corresponds to (the inherently symmetric) ≡L is L-equisimilarity: d1 and d2 are L-equisimilar, written d1 ∼L d2, if d1 ≤L d2 and d2 ≤L d1.

Example 2. In Figure 3 (R), d1 ∼EL d2, the EL-simulations are indicated by the dashed arrows. But d1 ̸∼ALC d2.

It is known from modal logic that ≡ALC ⊇ ∼ALC [Goranko and Otto, 2007], but that the converse holds only for certain classes of interpretations, called Hennessy-Milner classes, such as the class of all interpretations of finite outdegree. For our purposes, we need a class such that (i) ≡L ⊆ ∼L holds in this class, for all L ∈ DL and (ii) every interpretation is elementary equivalent (indistinguishable by FO sentences) to an interpretation in the class. These conditions are satisfied by the class of all ω-saturated interpretations, as known from classical model theory [Chang and Keisler, 1990] and defined in full detail in the long version. For the reader, it is most important that this class satisfies the above Conditions (i) and (ii). It can be seen that every finite interpretation and modally saturated interpretation in the sense of [Goranko and Otto, 2007] is ω-saturated.

Theorem3. Let L ∈ DL and (I1, d1) and (I2, d2) be objects.

1. If d1 ∼L d2, then d1 ≡L d2;
2. If d1 ≡L d2 and I1, I2 are ω-saturated, then d1 ∼L d2.

We now characterize concepts formulated in expressive DLs relative to FO. An FO-formula ϕ(x) is invariant under ∼L if for any two objects (I1, d1) and (I2, d2), from I1 |= ϕ[d1] and d1 ∼L d2 it follows that I2 |= ϕ[d2].

Theorem 4. Let L ∈ ExpDL and ϕ(x) an FO-formula. Then the following conditions are equivalent:

1. there exists an L-concept C such that C ≡ ϕ(x);
2. ϕ(x) is invariant under ∼L.

For ALC, this result is exactly van Benthem's characterization of modal formulae as the bisimulation invariant fragment of FO [Goranko and Otto, 2007]. For the modal logic variant of ALCQ, a similar, though more complex, characterization has been given in [de Rijke, 2000].

Concept definability in the lightweight DLs EL and DLLitehorn cannot be characterized exactly as in Theorem 3. In fact, one can show that invariance under ∼EL characterizes FO-formulae equivalent to Boolean combinations of ELconcepts, and invariance under ∼DL-Litehorn characterizes FOformulae equivalent to DL-Litebool-concepts, see [Artale et al., 2009]. To fix this problem, we switch from ∼L to ≤L and additionally require the FO-formula ϕ(x) to be preserved under direct products. Intuitively, the first modification addresses the restricted use of negation and the second one the lack of disjunction in EL and DL-Litehorn.

Let Ii, i ∈ I, be a family of interpretations. The (direct) product ∏i∈I Ii is the interpretation defined as follows:

Note that products are closely related to Horn logic, both in the case of full FO [Chang and Keisler, 1990] and modal logic [Sturm, 2000]. An FO-formula ϕ(x) is preserved under products if for all families (Ii)i∈I of interpretations and all ¯ d ∈ Δ∏ Ii with Ii |= ϕ[ ¯ di] for all i ∈ I, we have ∏i∈I Ii, |= ϕ[ ¯ d]. This notion is adapted in the obvious way to FO sentences. For L ∈ {EL, DL-Litehorn}, an FO-formula ϕ(x) is preserved under ≤L if (I1, d1) ≤L (I2, d2) and I1 |= ϕ[d1] imply I2 |= ϕ[d2].

Theorem 5. Let L ∈ {EL,DL-Litehorn} and ϕ(x) an FOformula. Then the following conditions are equivalent:

1. there exists an L-concept C such that C ≡ ϕ(x);
2. ϕ(x) is preserved under ≤L and under products.

Example 6. In Figure 4, di ∈ (∃r.A1⊔∃r.A2)Ii for i = 1, 2, but (d1, d2) ̸∈ (∃r.A1 ⊔ ∃r.A2)I1×I2 . Thus, disjunctions of EL-concepts are not preserved under products.

It is known that an FO-formula is preserved under products in the above sense iff it is preserved under binary products (where I has cardinality 2) [Chang and Keisler, 1990]. Likewise (and because of that), all results stated in this paper hold both for unrestricted produces and for binary ones.

4 Characterizing TBoxes, Expressive DLs

A natural first idea for lifting Theorem 4 from the concept level to the level of TBoxes is to replace the 'local' relations ∼L with their 'global' counterpart ∼gL, i.e., I1 ∼gL I2 iff for all d1 ∈ ΔI1 there exists d2 ∈ ΔI2 with (I1, d1) ∼L (I2, d2) and vice versa. It turns out that, in this way, we characterize Boolean L-TBoxes rather than L-TBoxes for all L ∈ ExpDL, where a Boolean L-TBox is an expression built up from Lconcept inclusions and the Boolean operators ¬, ∧, ∨. The proof exploits compactness and Theorem 3.

Theorem 7. Let L ∈ ExpDL and ϕ an FO-sentence. Then the following conditions are equivalent:

1. there exists a Boolean L-TBox T such that T ≡ ϕ;
2. ϕ is invariant under ∼gL.

To characterize TBoxes rather than Boolean TBoxes, we thus need to strengthen the conditions on ϕ. We first consider DLs without nominals. Let (Ii)i∈I be a family of interpretations. The union ∑i∈I Ii is defined by setting

• Δ∑i∈I Ii = ⋃i∈I ΔIi ;
• X∑i∈I Ii = ⋃i∈I XIi for X ∈ NC ∪NR.

If ΔIi ∩ ΔIj = ∅ for all distinct i, j ∈ I, then ∑i∈I Ii is a disjoint union. An FO-sentence ϕ is invariant under disjoint unions if for all families (Ii)i∈I of interpretations with pairwise disjoint domains, we have ∑i∈I Ii |= ϕ iff Ii |= ϕ for all i ∈ I. Similar to products, one can show that an FOsentence is invariant under disjoint unions iff it is invariant under binary disjoint unions.

Example 8. Examples of Boolean TBoxes not invariant under disjoint unions are (i) ϕ1 = (⊤ ⊑ A) ∨ (⊤ ⊑ B), since the disjoint union I of interpretations I1, I2 with AI1 = ΔI1 , BI1 = ∅, and, respectively, BI2 = ΔI2 , AI2 = ∅ is not a model of ϕ1; and (ii) ϕ2 = ¬(⊤ ⊑ A), since I is a model of ϕ2, but I1 is not.

Theorem 9. Let L ∈ ExpDL not contain nominals and ϕ be an FO-sentence. The following conditions are equivalent:

1. there exists a L-TBox T such that T ≡ ϕ;
2. ϕ is invariant under ∼gL and disjoint unions.

Proof. (sketch) The direction 1 ⇒ 2 is straightforward based on Theorem 3, Point 1. For the converse, let ϕ be invariant under ∼gL and disjoint unions and consider the set cons(ϕ) of all L-concept inclusions C ⊑ D such that ϕ |= C ⊑ D. We are done if we can show that cons(ϕ) |= ϕ: by compactness, one can find a finite T ⊆ cons(ϕ) with T |= ϕ, thus T is the desired L-TBox. Assume to the contrary that cons(ϕ) ̸|= ϕ. Our aim is to construct ω-saturated interpretations I - and I + such that I - ̸|= ϕ, I + |= ϕ, and for all d1 ∈ ΔI1 there exists d2 ∈ ΔI2 with (I1, d1) ≡L (I2, d2) and vice versa. By Theorem 3, this implies I - ∼gL I +, in contradiction to ϕ being invariant under ∼gL. For each L-concept inclusion C ⊑ D /∈ cons(ϕ), take a model IC̸⊑D of ϕ that refutes C ⊑ D. Then I + is defined as the disjoint union of all IC̸⊑D and I - is defined as the disjoint union of I + with a model of cons(ϕ) ∪ {¬ϕ}. It follows from invariance of ϕ under disjoint unions that I - ̸|= ϕ and I + |= ϕ. Moreover, I - and I + satisfy the same L-concept inclusions. Using the condition that L ∈ ExpDL, one can now show that ω-saturated interpretations that are elementary equivalent to I + and I - are as required. ❏

In a modal logic context, disjoint unions have first been used to characterize global consequence in [de Rijke and Sturm, 2001]. We exploit the purely model-theoretic characterizations given in Theorems 7 and 9 to obtain an easy, worst-case optimal algorithm deciding whether a Boolean TBox is equivalent to a TBox.

Theorem 10. Let L ∈ ExpDL not contain nominals. Then it is EXPTIME-complete to decide whether a Boolean L-TBox is invariant under disjoint unions (equivalently, whether it is equivalent to an L-TBox).

Proof. (sketch) The proof is by mutual reduction with the unsatisfiability problem for Boolean L-TBoxes, which is EXPTIME-complete in all cases [Baader et al., 2003]. We focus on the upper bound. Let ϕ be a Boolean L-TBox. For a concept name A, denote by ϕA the relativization of ϕ to A, i.e., a Boolean TBox such that any interpretation I is a model of ϕA iff the restriction of I to the domain AI is a model of ϕ. Take fresh concept names A1, A2 and let χ be the conjunction of A1 ⊓A2 ⊑ ⊥, ⊤ ⊑ A1 ⊔A2, Ai ⊑ ∀r.Ai, ¬(Ai ⊑ ⊥), for all role names r in ϕ and i ∈ {1, 2}, expressing that I is partitioned into two disjoint and unconnected parts, identified by A1 and A2. Then ϕ is invariant under binary disjoint unions iff the Boolean L-TBox χ → (ϕA1 ∧ ϕA2 ↔ ϕ) is a tautology. ❏

A further algorithmic application of Theorem 9 and of other characterizations that we will establish later is based on the following notion.

Definition 11 (TBox-rewritability). Let L1,L2 ∈ DL. A TBox T is L1-rewritable if it is equivalent to some L1-TBox. Then L1-to-L2 TBox-rewritability is the problem to decide whether a given L1-TBox is L2-rewritable.

If L1,L2 ∈ ExpDL do not contain nominals, then it follows from Theorem 9 that an L1-TBox T is L2-rewritable iff T it is invariant under ∼gL2 . This provides a way to obtain decision procedures for TBox-rewritability, which we explore for the first few steps in this paper: we consider ALCI-to-ALC rewritability in this section, and ALC-to-EL and ALCI-toDL-Lite rewritability in the subsequent one. The basis of the algorithms is that a TBox T is not L2-rewritable iff there are two interpretations related by ∼gL2 such that one is a model of T , but the other one is not.

Example 12. A typical rewriting between ALCI and ALC are range restrictions, which can be expressed by ∃r-.⊤ ⊑ B in ALCI and rewritten as ⊤ ⊑ ∀r.B in ALC. Contrastingly, the ALCI-TBox T = {∃r-.⊤⊓∃s-.⊤ ⊑ B} is not invariant under ∼gALC : in Figure 5, T is satisfied in I2, but not in I1 (where BI1 = BI2 = ∅). Thus, T is not equivalent to any ALC-TBox.

The following result is proved by a non-trivial refinement of the method of type elimination known from complexity proofs in modal and description logic. We leave a matching lower complexity bound as an open problem for now.

Theorem 13. ALCI-to-ALC TBox rewritability is decidable in 2-EXPTIME.

Theorem 9 excludes DLs with nominals since it is not clear how to interpret nominals in a disjoint union such that they are still singletons. In the following, we devise a relaxed variant of disjoint unions that respects nominals. For simplicity, we only consider DLs with nominals that have inverse roles as well (our approach can also be made to work otherwise, but becomes more technical).

A component of an interpretation I is a set D ⊆ ΔI that is closed under neighbors, i.e., if d ∈ D and (d, d′ ) ∈ ⋃r∈NR rI ∪ (r-)I , then d′ ∈ D. A component interpretation of I is the restriction J of I to some domain ΔJ ⊆ ΔI that is a component of I, i.e., AJ = AI ∩ ΔJ for all A ∈ NC, rJ = rI ∩ (ΔJ ×ΔJ ) for all r ∈ NR, and aJ = aI for a ∈ NI if aI ∈ ΔJ ; otherwise, aJ is simply undefined. We denote by Nom(J) the set of individual names interpreted by J . Now let (Ji)i∈I be a family of component interpretations such that

• ⋃i∈I Nom(Ji) = NI;
• Nom(Ji) ∩ Nom(Jj) = ∅ for all i ̸= j.

Then the nominal disjoint union of (Ji)i∈I, denoted ∑nom i∈I Ji, is the interpretation obtained by taking the disjoint union of (Ji)i∈I and then interpreting each a ∈ NI as aJi for the unique i ∈ I with aJi defined.

An FO-sentence ϕ is invariant under nominal disjoint unions if the following conditions hold for all families (Ii, Ji)i∈I with Ii an interpretation and Ji a component interpretation of Ii, for all i ∈ I:

• (a) if Ii is a model of ϕ for all i ∈ I, then so is ∑nom i∈I Ji;
• (b) if ∑nom i∈I Ji is a model of ϕ and Ii0 = Ji0 for some i0 ∈ I, then Ii0 is a model of ϕ.

Note that, in Condition (b), Ii0 = Ji0 implies that Nom(Ji0 ) is the set of all individual names, but not necessarily that ∑nom i∈I Ji = Ji0 . We can now characterize TBoxes formulated in expressive DLs with nominals.

Theorem 14. Let L ∈ {ALCIO,ALCQIO} and ϕ be an FO-sentence. Then the following conditions are equivalent:

1. there exists an L-TBox T such that T ≡ ϕ;
2. ϕ is invariant under ∼gL and nominal disjoint unions.

Example 15. Condition (a) of nominal disjoint unions can be used to show that ϕ = A(a) ∨ A(b) cannot be rewritten as an ALCQIO-TBox. To see this, observe that I1 and I2 of Figure 6 satisfy ϕ and ∑nom i=1,2 Ji does not satisfy ϕ.

Similar to the proof of Theorem 10, one can use relativization to reduce the problem of checking invariance under nominal disjoint unions of Boolean L-TBoxes to the unsatisfiability problem for Boolean L-TBoxes (which is EXPTIME-complete for ALCIO and coNEXPTIME-complete for ALCQIO [Baader et al., 2003]):

Theorem 16. It is EXPTIME-complete to decide whether a Boolean ALCIO-TBox is invariant under nominal disjoint unions (equivalently, whether it is equivalent to an ALCIOTBox). The problem is coNEXPTIME-complete for Boolean ALCQIO-TBoxes.

5 Characterizing TBoxes, Lightweight DLs

We characterize TBoxes formulated in EL and members of the DL-Lite families. We start with an analogue of Theorem 5: since the considered DLs are 'Horn' in nature, we add products to the closure properties identified in Section 4 and refine our proofs accordingly.

Theorem 17. Let L ∈ {EL,DL-Litehorn} and let ϕ be an FO-sentence. The following conditions are equivalent:

1. ϕ is equivalent to an L-TBox;
2. ϕ is invariant under ∼gL and disjoint unions, and preserved under products.

Proof. (sketch) In principle, we follow the strategy of the proof of Theorem 9. A problem is posed by the fact that, unlike in the case of expressive DLs, two ω-saturated interpretations I - and I + that satisfy the same L-CIs need not satisfy I - ≡gL I + (e.g. when I - consists of three elements that satisfy A ⊓ ¬B, and B ⊓ ¬A, and ¬A ⊓ ¬B, respectively, and I + consists of two elements that satisfy A ⊓ ¬B and B ⊓ ¬A, respectively). To deal with this, we ensure that I - and I + satisfy the same disjunctive L-CIs, i.e., CIs of the form C ⊑ D1 ⊔ · · · ⊔ Dn with C, D1, . . . , Dn L-concepts; this suffices to prove I - ≡g I + as required. The construction of I - is essentially as in the proof of Theorem 9 while the construction of I + uses products to bridge the gap between L-CIs and disjunctive L-CIs. ❏

We apply Theorem 17 to TBox rewritability, starting with the ALC-to-EL case. By Theorems 9 and 17, an ALC-TBox is equivalent to some EL-TBox iff it is invariant under ∼gEL and preserved under binary products. The following theorem, the proof of which is rather involved, establishes the complexity of both problems.

Theorem 18. Invariance of ALC-TBoxes under ∼gEL is EXPTIME-complete. Preservation of ALC-TBoxes under products is coNEXPTIME-complete.

From Theorems 18 and 17 we obtain:

Theorem 19. ALC-to-EL TBox rewritability is in coNEXPTIME.

One can easily show EXPTIME-hardness of ALC-to-EL TBox rewritability by reduction of satisfiability of ALCTBoxes. Namely, T is satisfiable iff T ∪{A ⊑ ∀r.B} cannot be rewritten into an EL-TBox, where A,B, r do not occur in T . Finding a tight bound remains open.

We now consider ALCI-to-DL-Litehorn TBox rewritability and establish EXPTIME-completeness. In contrast to ALC-to-EL rewritability, where it is not clear whether or not the computationally expensive check for preservation under products can be avoided, here a rather direct approach is possible that relies only on deciding invariance under ∼DL-Litehorn .

Theorem 20. ALCI-to-DL-Litehorn-TBox rewritability is EXPTIME-complete.

Proof. (sketch) First decide in EXPTIME whether T is invariant under ∼DL-Litehorn . If not, then T is not equivalent to any DL-Litehorn-TBox. If yes, check, in exponential time, whether for every B1 ⊓ · · · ⊓ Bn ⊑ B′1 ⊔ · · · ⊔ B′m that follows from T with all Bi,B′i basic concepts, there exists j such that B1 ⊓ · · · ⊓Bn ⊑ B′j follows from T . T is equivalent to some DL-Litehorn-TBox iff this is the case. ❏

The original DL-Lite dialects do not admit conjunction as a concept constructor, or only to express disjointness constraints. More precisely, a DL-Litecore-TBox is a finite set of inclusions B1 ⊑ B2, where B1,B2 are basic DL-Lite concepts as defined in Section 2. A DL-Litedcore -TBox admits, in addition, inclusions B1 ⊓ B2 ⊑ ⊥ expressing disjointness of B1 and B2. To characterize TBoxes formulated in DLLitecore and DL-Litedcore , we additionally require preservation under (non-disjoint) unions and compatible unions, respectively. The latter are unions of interpretations (Ii)i∈I that can be formed only if the family (Ii)i∈I is compatible, i.e., for any d ∈ ΔIi ∩ ΔIj and basic DL-Lite concepts B1,B2 such that d ∈ BIi 1 ∩BIj 2 there exists Iℓ with (B1⊓B2)Iℓ ̸= ∅. Preservation of FO-sentences under (compatible) unions is defined in the obvious way. The proof of the following theorem is similar to that of Theorem 17, except that the construction of I + is yet a bit more intricate.

Theorem 21. Let ϕ be an FO-sentence. Then the following conditions are equivalent:

1. ϕ is equivalent to a DL-Litecore-TBox (DL-Litedcore -TBox);
2. ϕ is invariant under ∼gDL-Litehorn and disjoint unions, and preserved under products and unions (compatible unions).

Note that it is not possible to strengthen Condition 2 of Theorem 21 by requiring ϕ to be invariant under unions as this results in failure of the implication 1 ⇒ 2.

Because of the fact that there are only polynomially many concept inclusions over any finite signature, TBox rewritability into DL-Litecore and DL-Litedcore is a comparably simple problem and semantic characterizations are less fundamental here than for more expressive DLs. In fact, for L ∈ ExpDL that contains inverse roles, one can reduce L-to-DL-Litecore rewritability to Boolean L-TBox unsatisfiability. Conversely (and trivially), L-TBox unsatisfiability can be reduced to L-to-DL-Litecore TBox rewritability. As for all expressive DLs in this paper the complexity of TBox satisfiability and Boolean TBox satisfiability coincide, this yields tight complexity bounds. The same holds for DL-Litedcore . For a related study of approximation in DL-Lite, see [Botoeva et al., 2010].

6 Discussion

We believe that the results established in this paper have many potential applications in areas where the expressive power of TBoxes plays a central role, such as TBox approximation and modularity. We also believe that the problem of TBox rewritability, studied here as an example application of our characterization results, is interesting in its own right. A more comprehensive study, including the actual computation of rewritten TBoxes, remains as future work.

The DLs standardized as OWL 2 and its profiles have additional expressive power compared to the 'core DLs' studied in this paper. While full OWL 2 is probably too complex to admit really succinct characterizations of the kind established here, some extensions are possible as follows: each of Theorems 9, 14, and 17 still holds when the admissible interpretations are restricted to some class that is definable by an FO-sentence preserved under the notion of (disjoint) union and product used in that theorem. This captures many features of OWL such as transitive roles, role hierarchy axioms, and even role inclusion axioms.

Acknowledgments. This work was supported by the DFG SFB/TR 8 "Spatial Cognition".