Foundations for Uniform Interpolation and Forgetting in Expressive Description Logics

1 Introduction

In Description Logic (DL), a TBox or ontology is a logical theory that describes the conceptual knowledge of an application domain using a set of appropriate predicate symbols. For example, in the domain of universities and students, the predicate symbols could include the concept names Uni, Undergrad, and Grad, and the role name has student. When working with an ontology, it is often useful to eliminate some of the used predicates while retaining the meaning of all remaining ones. For example, when re-using an existing ontology in a new application, then typically only a very small fraction of the predicates is of interest. Instead of re-using the whole ontology, one can thus use the potentially much smaller ontology that results from an elimination of the nonrelevant predicates. Another reason for eliminating predicates is predicate hiding, i.e., an ontology is to be published, but some part of it should be concealed from the public because it is confidential [Grau and Motik, 2010]. Finally, one can view the result of predicate elimination as an approach to ontology summary: the resulting, smaller and more focussed ontology summarizes what the original ontology says about the remaining predicates.

The idea of eliminating predicates has been studied in AI under the name of forgetting a signature (set of predicates) Σ, i.e., rewriting a knowledge base K such that it does not use predicates from Σ anymore and still has the same logical consequences that do not refer to predicates from Σ [Reiter and Lin, 1994]. In propositional logic, forgetting is also known as variable elimination [Lang et al., 2003]. In mathematical logic, forgetting has been investigated under the dual notion of uniform interpolation w.r.t. a signature Σ, i.e., rewriting a formula ϕ such that it uses only predicates from Σ and has the same logical consequences formulated only in Σ. The result of this rewriting is then the uniform interpolant of ϕ w.r.t. Σ. This notion can be seen as a generalization of the more widely known Craig interpolation.

Due to the various applications briefly discussed above, forgetting und uniform interpolation receive increased interest also in a DL context [Eiter et al., 2006; Wang et al., 2010; 2009b; 2008; Kontchakov et al., 2010; Konev et al., 2009]. Here, the knowledge base K resp. formula ϕ is replaced with a TBox T . In fact, uniform interpolation is rather well-understood in lightweight DLs such as DL-Lite and EL: there, uniform interpolants of a TBox T can often be expressed in the DL in which T is formulated [Kontchakov et al., 2010; Konev et al., 2009] and practical experiments have confirmed the usefulness and feasibility of their computation [Konev et al., 2009]. The situation is different for 'expressive' DLs such as ALC and its various extensions, where much less is known. There is a thorough understanding of uniform interpolation on the level of concepts, i.e., computing uniform interpolants of concepts instead of TBoxes [ten Cate et al., 2006; Wang et al., 2009b], which is also what the literature on uniform interpolants in modal logic is about [Visser, 1996; Herzig and Mengin, 2008]. On the TBox level, a basic observation is that there are very simple ALC-TBoxes and signatures Σ such that the uniform interpolant of T w.r.t. Σ cannot be expressed in ALC (nor in first-order predicate logic) [Ghilardi et al., 2006]. A scheme for approximating (existing or non-existing) interpolants of ALC-TBoxes was devised in [Wang et al., 2008]. In [Wang et al., 2010], an attempt is made to improve this to an algorithm that computes uniform interpolants of ALC-TBoxes in an exact way, and also decides their existence (resp. expressibility in ALC). Unfortunately, that algorithm turns out to be incorrect.

The aim of this paper is to lay foundations for uniform interpolation in ALC and other expressive DLs, with a focus on (i) model-theoretic characterizations of uniform interpolants and their existence; (ii) deciding the existence of uniform interpolants and computing them in case they exist; and (iii) analyzing the size of uniform interpolants. Clearly, these are fundamental steps on the way towards the computation and usage of uniform interpolation in practical applications. Regarding (i), we establish an intimate connection between uniform interpolants and the well-known notion of a bisimulation and characterize the existence of interpolants in terms of the existence of models with certain properties based on bisimulations. For (ii), our main result is that deciding the existence of uniform interpolants is 2-EXPTIME-complete, and that methods for computing uniform interpolants on the level of concepts can be lifted to the TBox level. Finally, regarding (iii) we prove that the size of uniform interpolants is at most triple exponential in the size of the original TBox (upper bound), and that, in general, no shorter interpolants can be found (lower bound). In particular, this shows that the algorithm from [Wang et al., 2010] is flawed as it always yields uniform interpolants of at most double exponential size. Our methods, which are a mix of model-theory and automata-theory, also provide model-theoretic characterizations of conservative extensions, which are closely related to uniform interpolation [Ghilardi et al., 2006]. Moreover, we use our approach to reprove the 2-EXPTIME upper bound for deciding conservative extensions from [Ghilardi et al., 2006], in an alternative and argueably more transparent way.

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

2 Getting Started

We introduce the description logic ALC and define uniform interpolants and the dual notion of forgetting. Let NC and NR be disjoint and countably infinite sets of concept and role names. ALC concepts are formed using the syntax rule

where A ∈ NC and r ∈ NR. The concept constructors ⊥, ⊔, and ∀r.C are defined as abbreviations: ⊥ stands for ¬⊤, C ⊔ D for ¬(¬C ⊓ ¬D) and ∀r.C abbreviates ¬∃r.¬C. A TBox is a finite set of concept inclusions C ⊑ D, where C, D are ALC-concepts. We use C ≡ D as abbreviation for the two inclusions C ⊑ D and D ⊑ C.

The semantics of ALC-concepts is given in terms of interpretations I = (ΔI , ·I ), where ΔI is a non-empty set (the domain) and ·I is the interpretation function, assigning to each A ∈ NC a set AI ⊆ ΔI , and to each r ∈ NR a relation rI ⊆ ΔI × ΔI . The interpretation function is inductively extended to concepts as follows:

An interpretation I satisfies an inclusion C ⊑ D if CI ⊆ DI , and I is a model of a TBox T if it satisfies all inclusions in T . A concept C is subsumed by a concept D relative to a TBox T (written T |= C ⊑ D) if every model I of T satisfies the inclusion C ⊑ D. We write T |= T ′ to indicate that T |= C ⊑ D for all C ⊑ D ∈ T ′ .

A set Σ ⊆ NC ∪ NR of concept and role names is called a signature. The signature sig(C ) of a concept C is the set of concept and role names occurring in C, and likewise for the signature sig(C ⊑ D) of an inclusion C ⊑ D and sig(T ) of a TBox T . A Σ-TBox is a TBox with sig(T ) ⊆ Σ, and likewise for Σ-inclusions and Σ-concepts.

We now introduce the main notions studied in this paper: uniform interpolants and conservative extensions.

Definition 1. Let T , T ′ be TBoxes and Σ a signature. T and T ′ are Σ-inseparable if for all Σ-inclusions C ⊑ D, we have T |= C ⊑D iff T ′ |= C ⊑ D. We call

• T ′ a conservative extension of T if T ′ ⊇ T and T and T ′ are Σ-inseparable for Σ = sig(T ).
• T a uniform Σ-interpolant of T ′ if sig(T ) ⊆ Σ ⊆ sig(T ′ ) and T and T ′ are Σ-inseparable.

Note that uniform Σ-interpolants are unique up to logical equivalence, if they exist.

The notion of forgetting as investigated in [Wang et al., 2010] is dual to uniform interpolation: a TBox T ′ is the result of forgetting about a signature Σ in a TBox T if T ′ is a uniform sig(T ) \ Σ-interpolant of T .

Example 2. Let T consist of the inclusions

1. Uni ⊑ ∃has st.Undergrad ⊓ ∃has st.Grad
2. Uni ⊓Undergrad ⊑ ⊥ (3) Uni ⊓Grad ⊑ ⊥
3. Undergrad ⊓ Grad ⊑ ⊥.

Then the TBox that consists of (2) and

Uni ⊑ ∃has st.Undergrad ⊓ ∃has st.(¬Undergrad ⊓¬Uni)

• is the result of forgetting {Grad}. Additionally forgetting Undergrad yields the TBox {Uni ⊑ ∃has st.¬Uni}.

The following examples will be used to illustrate our characterizations. Proofs are provided once we have developed the appropriate tools.

Example 3. In the following, we always forget {B}.

• (i) Let T1 = {A ⊑ ∃r.B ⊓ ∃r.¬B} and Σ1 = {A, r}. Then T ′ 1 = {A ⊑ ∃r.⊤} is a uniform Σ1-interpolant of T1.
• (ii) Let T2 = {A ≡ B ⊓ ∃r.B} and Σ2 = {A, r}. Then T ′ 2 = {A ⊑ ∃r.(A ⊔ ¬∃r.A)} is a uniform Σ2-interpolant of T2.

(iii) For T3 = {A ⊑ B, B ⊑ ∃r.B} and Σ3 = {A, r}, there is no uniform Σ3-interpolant of T3.

(iv) For T4 = {A ⊑ ∃r.B, A0 ⊑ ∃r.(A1 ⊓ B), E ≡ A1 ⊓ B ⊓ ∃r.(A2 ⊓ B)} and Σ4 = {A, r,A0,A1,E}, there is no uniform Σ4-interpolant of T4. Note that T4 is of a very simple form, namely an acyclic EL-TBox, see [Konev et al., 2009].

Bisimulations are a central tool for studying the expressive power of ALC, and play a crucial role also in our approach to uniform interpolants. We introduce them next. A pointed interpretation is a pair (I, d) that consists of an interpretation I and a d ∈ ΔI .

Definition 4. Let Σ be a finite signature and (I1, d1), (I2, d2) pointed interpretations. A relation S ⊆ ΔI1 × ΔI2 is a Σbisimulation between (I1, d1) and (I2, d2) if (d1, d2) ∈ S and for all (d, d′ ) ∈ S the following conditions are satisfied:

1. d ∈ AI1 iff d′ ∈ AI2 , for all A ∈ Σ∩NC;
2. if (d, e) ∈ rI1 , then there exists e′ ∈ ΔI2 such that (d′ , e′ ) ∈ rI2 and (e, e′ ) ∈ S, for all r ∈ Σ∩NR;
3. if (d′ , e′ ) ∈ rI2 , then there exists e ∈ ΔI1 such that (d, e) ∈ rI1 and (e, e′ ) ∈ S, for all r ∈ Σ∩NC.
4. (I1, d1) and (I2, d2) are Σ-bisimilar, written (I1, d1) ∼Σ (I2, d2), if there exists a Σ-bisimulation between them.

We now state the main connection between bisimulations and ALC, well-known from modal logic [Goranko and Otto, 2007]. Say that (I1, d1) and (I2, d2) are ALCΣ-equivalent, in symbols (I1, d1) ≡Σ (I2, d2), if for all Σ-concepts C, d1 ∈ C I1 iff d2 ∈ C I2 . An interpretation I has finite outdegree if {d′ | (d, d′ ) ∈ ⋃r∈NR rI } is finite, for all d ∈ ΔI .

Theorem 5. For all pointed interpretations (I1, d1) and (I2, d2) and all finite signatures Σ, (I1, d1) ∼Σ (I2, d2) implies (I1, d1) ≡Σ (I2, d2); the converse holds for all I1, I2 of finite outdegree.

Bisimulations enable a purely semantic characterization of uniform interpolants. For a pointed interpretation (I, d), we write (I, d) |= ∃∼Σ .T when (I, d) is Σ-bisimilar to some pointed interpretation (J , d′ ) with J a model of T . The notation reflects that what we express here can be understood as a form of bisimulation quantifier, see [French, 2006].

Theorem 6. Let T be a TBox and Σ ⊆ sig(T ). A Σ-TBox TΣ is a uniformΣ-interpolant of T iff for all interpretations I,

For I of finite outdegree, one can prove this result by employing compactness arguments and Theorem 5. To prove it in its full generality, we need the automata-theoretic machinery introduced in Section 4. We illustrate Theorem 6 by sketching a proof of Example 3(i). Correctness of 3(ii) is proved in the appendix, while 3(iii) and 3(iv) are addressed in Section 3. An interpretation I is called a tree interpretation if the undirected graph (ΔI , ⋃r∈NR rI ) is a (possibly infinite) tree and rI ∩ sI = ∅ for all distinct r, s ∈ NR.

Example 7. Let T1 = {A ⊑ ∃r.B ⊓ ∃r.¬B}, Σ1 = {A, r},

The first 'iff' relies on the fact that unraveling an interpretation into a tree interpretation preserves bisimularity, the second one on the fact that bisimulations are oblivious to the duplication of successors, and the third one on a reinterpretation of B /∈ Σ1 in J .

Theorem 6 also yields a characterization of conservative extensions in terms of bisimulations, which is as follows.

Theorem 8. Let T , T ′ be TBoxes. Then T ∪ T ′ is a conservative extension of T iff for all interpretations I, I |= T ⇒ for all d ∈ ΔI , (I, d) |= ∃∼Σ .T ′ where Σ = sig(T ).

3 Characterizing Existence of Interpolants

If we admit TBoxes that are infinite, then uniform Σinterpolants always exist: for any TBox T and signature Σ, the infinite TBox T ∞ Σ that consists of all Σ-inclusions C ⊑D with T |= C ⊑ D is a uniform Σ-interpolant of T . To refine this simple observation, we define the role-depth rd(C ) of a concept C to be the nesting depth of existential restrictions in C. For every finite signature Σ and m ≥ 0, one can fix a finite set Cm f (Σ) of Σ-concepts D with rd(D) ≤ m such that every Σ-concept C with rd(C ) ≤ m is equivalent to some D ∈ Cm f (Σ). Let

Clearly, T ∞ Σ is equivalent to ⋃m≥0 TΣ,m suggesting that if a uniform interpolant exists, it is one of the TBoxes TΣ,m. In fact, it is easy to see that the following are equivalent (this is similar to the approximation of uniform interpolants in [Wang et al., 2008]):

• (a) there does not exist a uniformΣ-interpolant of T ;
• (b) no TΣ,m is a uniformΣ-interpolant of T ;
• (c) for all m≥ 0 there is a k >m such that TΣ,m ̸|= TΣ,k.

Our characterization of the (non)-existence of uniform interpolants is based on an analysis of the TBoxes TΣ,m. For an interpretation I, d ∈ ΔI , and m ≥ 0, we use I ≤m(d) to denote the m-segment generated by d in I, i.e., the restriction of I to those elements of ΔI that can be reached from d in at most m steps in the graph (ΔI , ⋃r∈NR rI ). Using the definition of TΣ,m, Theorem 5, and the fact that every msegment can be described up to bisimulation using a concept of role-depth m, it can be shown that an interpretation I is a model of TΣ,m iff each of I's m-segments is Σ-bisimilar to an m-segment of a model of T . Thus, if TΣ,m is not a uniform interpolant, then this is due to a problem that cannot be 'detected' by m-segments, i.e., some Σ-part of a model of T that is located before an m-segment can pose constraints on Σ-parts of the model after that segment, where 'before' and 'after' refer to reachability in (ΔI , ⋃r∈NR rI ).

The following result describes this in an exact way. Together with the equivalence of (a) and (b) above, it yields a first characterization of the existence of uniform interpolants. ρI denotes the root of a tree interpretation I, I ≤m abbreviates I ≤m(ρI ), and a Σ-tree interpretation is a tree interpretations that only interprets predicates fromΣ.

Theorem 9. Let T be a TBox, Σ ⊆ sig(T ), and m ≥ 0. Then TΣ,m is not a uniformΣ-interpolant of T iff

(∗m) there exist two Σ-tree interpretations, I1 and I2, of finite outdegree such that

1. For all successors d of ρI2 : (I2, d) |=

Intuitively, Points 1 and 2 ensure that I ≤m 1 = I ≤m 2 is an m-segment of a model of TΣ,m, Points 2 and 3 express that in models of T , the Σ-part after the m-segment is constrained in some way, and Point 4 says that this is due to ρI1 and ρI2 , i.e., the constraint is imposed 'before' the m-segment. The following example demonstrates how Theorem 9 can be used to prove non-existence of uniform interpolants.

Example 10. Let T3 = {A ⊑ B,B ⊑ ∃r.B} and Σ3 = {A, r} as in Example 3(iii). We show that (∗m) holds for all m and thus, there is no uniform Σ3-interpolant of T3. Example 3(iv) is treated in the long version.

Let m ≥ 0. Set I1 = ({0, 1, . . .}, AI1 , rI1 ), where AI1 = {0} and rI1 = {(n, n + 1) | n ≥ 0}, and let I2 be the restriction of I1 to {0, . . . ,m}. Then (1) I ≤m 1 = I ≤m 2 ; (2) (I1, 0) |= ∃∼Σ3 T3 as the expansion of I1 by BI1 = {0, 1, . . .} is a model of T3; (3) (I2, 0) ̸|= ∃∼Σ3 T3 as there is no infinite r-sequence in I2 starting at 0; and (4) (I2, 1) |= ∃∼Σ3 T3 as the restriction of I2 to {1, . . . ,m} is a model of T3.

The next example illustrates another use of Theorem 9 by identifying a class of signatures for which uniform interpolants always exist. Details are given in the long version.

Example 11 (Forgetting stratified concept names). A concept name A is stratified in T if all occurrences of A in concepts from conc(T ) = {C,D | C ⊑ D ∈ T } are exactly in nesting depth n of existential restrictions, for some n ≥ 0. Let T be a TBox and Σ a signature such that sig(T ) \ Σ consists of stratified concept names only, i.e., we want to forget a set of stratified concept names. Then the existence of a uniform Σ-interpolant of T is guaranteed; moreover, TΣ,m is such an interpolant, where m = max{rd(C ) | C ∈ conc(T )}.

To turn Theorem 9 into a decision procedure for the existence of uniform interpolants, we prove that rather than testing (∗m) for all m, it suffices to consider a single number m. This yields the final characterization of the existence of uniform interpolants. We use |T | to denote the length of a TBox T , i.e., the number of symbols needed to write it.

Theorem 12. Let T be a TBox and Σ ⊆ sig(T ). Then there does not exist a uniformΣ-interpolant of T iff (∗M2 T +1) from Theorem 9 holds, where MT := 22|T | .

It suffices to show that (∗M2 T +1) implies (∗m) for all m ≥ M 2 T + 1. The proof idea is as follows. Denote by cl(T ) the closure under single negation and subconcepts of conc(T ). The type of some d ∈ ΔI in an interpretation I is

Many constructions for ALC (such as blocking in tableaux, filtrations of interpretations, etc.) exploit the fact that the relevant information about any element d in an interpretation is given by its type. This can be exploited e.g. to prove EXPTIME upper bounds as there are 'only' exponentially many distinct types. In the proof of Theorem 12, we make use of a 'pumping lemma' that enables us to transform any pair I1, I2 witnessing (∗M2 T +1) into a witness I ′1 , I ′2 for (∗m) when m ≥ M 2 T + 1. The construction depends on the relevant information about elements of ΔI1 and ΔI2 ; in contrast to standard constructions, however, types are not sufficient and must be replaced by extension sets ExtI (d), defined as

and capturing all ways in which the restiction of tpI (d) to Σ-concepts can be extended to a full type in models of T . As the number of such extension sets is double exponential in

|T | and we have to consider pairs (d1, d2) ∈ ΔI1 × ΔI2 , we (roughly) obtain a M 2 T bound. Details are in the long version.

We note that, by Theorem 12, the uniform Σ-interpolant of a TBox T exists iff T ∪TΣ,M2 T +1 is a conservative extension of TΣ,M2 T +1. With the decidability of conservative extensions proved in [Ghilardi et al., 2006], this yields decidablity of the existence of uniform interpolants. However, the size of TΣ,M2 T +1 is non-elementary, and so is the running time of the resulting algorithm. We next show how to improve this.

4 Automata Constructions / Complexity

We develop a worst-case optimal algorithm for deciding the existence of uniform interpolants in ALC, exploiting Theorem 12 and making use of alternating automata. As a byproduct, we prove the fundamental characterization of uniform interpolants in terms of bisimulation stated as Theorem 6 without the initial restriction to interpretations of finite outdegree. We also obtain a representation of uniform interpolants as automata and a novel, more transparent proof of the 2-EXPTIME upper bound for deciding conservative extensions originally established in [Ghilardi et al., 2006].

We use amorphous alternating parity tree automata in the style of Wilke [Wilke, 2001], which run on unrestricted interpretations rather than on trees, only. We call them tree automata as they are in the tradition of more classical forms of such automata. In particular, a run of an automaton is treeshaped, even if the input interpretation is not.

Definition 13 (APTA). An alternating parity tree automaton (APTA) is a tuple A = (Q, ΣN , ΣE, q0, δ, Ω), where Q is a finite set of states, ΣN ⊆ NC is the finite node alphabet, ΣE ⊆ NR is the finite edge alphabet, q0 ∈ Q is the initial state, δ : Q→mov(A), is the transition function with mov(A) = {true, false, A, ¬A, q, q ∧ q′ , q ∨ q′ , 〈r〉q, [r]q | A ∈ ΣN, q, q′ ∈ Q, r ∈ ΣE} the set of moves of the automaton, and Ω : Q→ is the priority function. H11934

Intuitively, the move q means that the automaton sends a copy of itself in state q to the element of the interpretation that it is currently processing, 〈r〉q means that a copy in state q is sent to an r-successor of the current element, and [r]q means that a copy in state q is sent to every r-successor.

It will be convenient to use arbitrary modal formulas in negation normal form when specifying the transition function of APTAs. The more restricted form required by Definition 13 can then be attained by introducing intermediate states. In subsequent constructions that involve APTAs, we will not describe those additional states explicitly. However, we will (silently) take them into account when stating size bounds for automata.

In what follows, a Σ-labelled tree is a pair (T, ℓ) with T a tree and ℓ : T → Σ a node labelling function. A path π in a tree T is a subset of T such that ε ∈ π and for each x ∈ π that is not a leaf in T , π contains one son of x.

Definition 14 (Run). Let (I, d0) be a pointed ΣN ∪ ΣEinterpretation and A = (Q, ΣN , ΣE, q0, δ, Ω) an APTA. A run of A on (I, d0) is a Q× ΔI -labelled tree (T, ℓ) such that ℓ(ε) = (q0, d0) and for every x ∈ T with ℓ(x) = (q, d):

• δ(q) ̸= false;

• if δ(q) = A (δ(q) = ¬A), then d ∈ AI (d /∈ AI );
• if δ(q) = q′ ∧ q′′ , then there are sons y, y′ of x with ℓ(y) = (q′ , d) and ℓ(y′ ) = (q′′ , d);
• if δ(q) = q′ ∨ q′′ , then there is a son y of x with ℓ(y) = (q′ , d) or ℓ(y′ ) = (q′′ , d);
• if δ(q) = 〈r〉q′ , then there is a (d, d′ ) ∈ rI and a son y of x with ℓ(y) = (q′ , d′ );
• if δ(q) = [r]q′ and (d, d′ ) ∈ rI , then there is a son y of x with ℓ(y) = (q′ , d′ ).

A run (T, ℓ) is accepting if for every path π of T , the maximal i ∈ with {x ∈ π | ℓ(x) = (q, d) with Ω(q) = i} infinite is even. We use L(A) to denote the language accepted by A, i.e., the set of pointed ΣN ∪ ΣE-interpretations (I, d) such that there is an accepting run of A on (I, d). H11934

Using the fact that runs are always tree-shaped, it is easy to prove that the languages accepted by APTAs are closed under ΣN ∪ΣE-bisimulations. It is this property that makes this automaton model particularly useful for our purposes. APTAs can be complemented in polytime in the same way as other alternating tree automata, and for all APTAs A1 and A2, one can construct in polytime an APTA that accepts L(A1)∩L(A2). Wilke shows that the emptiness problem for APTAs is EXPTIME-complete [Wilke, 2001].

We now show that uniform Σ-interpolants of ALC-TBoxes can be represented as APTAs, in the sense of the following theorem and of Theorem 6.

Theorem 15. Let T be a TBox and Σ ⊆ sig(T ) a signature. Then there exists an APTA AT ,Σ = (Q, Σ ∩ NC, Σ ∩ NR, q0, δ, Ω) with |Q| ∈ 2O(|T |) such that L(AT ,Σ) consists of all pointed Σ-interpretations (I, d) with (I, d) |= ∃∼Σ .T . AT ,Σ can be constructed in time 2p(|T |) , p a polynomial.

The construction of the automaton AT ,Σ from Theorem 15 resembles the construction of uniform interpolants in the μ-calculus using non-deterministic automata described in [D'Agostino and Hollenberg, 1998], but is transferred to TBoxes and alternating automata.

Fix a TBox T and a signature Σ and assume w.l.o.g. that T has the form {⊤ ⊑ CT }, with CT in negation normal form [Baader et al., 2003]. Recall the notion of a type introduced in Section 3. We use TP(T ) to denote the set of all types realized in some model of T , i.e., TP(T ) = {tpI (d) | I model of T , d ∈ ΔI }. Note that TP(T ) can be computed in time exponential in the size of T since concept satisfiability w.r.t. TBoxes is EXPTIME-complete in ALC [Baader et al., 2003]. Given t, t′ ∈ TP(T ) and r ∈ Σ, we write t ⇝r t′ if C ∈ t′ implies ∃r.C ∈ t for all ∃r.C ∈ cl(T ). Now define the automaton AT ,Σ := (Q, ΣN , ΣE, q0, δ, Ω), where

Here, the empty conjunction represents true and the empty disjunction represents false. The acceptance condition of the automaton is trivial, which (potentially) changes when we complement it subsequently. We prove in the appendix that this automaton satisfies the conditions in Theorem 15.

We now develop a decision procedure for the existence of uniform interpolants by showing that the characterization of the existence of uniform interpolants provided by Theorem 12 can be captured by APTAs, in the following sense.

Theorem 16. Let T be a TBox, Σ ⊆ sig(T ) a signature, and m ≥ 0. Then there is an APTA AT ,Σ,m = (Q, ΣN , ΣE, q0, δ, Ω) such that L(A) ̸= ∅ iff Condition (∗m) from Theorem 9 is satisfied. Moreover, |Q| ∈ O(2O(n) + log2 m) and |ΣN|, |ΣE| ∈ O(n + log m), where n = |T |.

The size of AT ,Σ,m is exponential in |T | and logarithmic in m. By Theorem 12, we can set m = 22|T | , and thus the size of AT ,Σ,m is exponential in |T |. Together with the EXPTIME emptiness test for APTAs, we obtain a 2-EXPTIME decision procedure for the existence of uniform interpolants. We construct AT ,Σ,m as an intersection of four APTAs, each ensuring one of the conditions of (∗m); building the automaton for Condition 2 involves complementation. The automaton AT ,Σ,m runs over an extended alphabet that allows to encode both of the interpretations I1 and I2 mentioned in (∗m), plus a 'depth counter' for enforcing Condition 1 of (∗m).

A similar, but simpler construction can be used to reprove the 2-EXPTIME upper bound for deciding conservative extensions established in [Ghilardi et al., 2006]. The construction only depends on Theorem 8, but not on the material in Section 3 and is arguably more transparent than the original one.

Theorem 17. Given TBoxes T and T ′ , it can be decided in time 2p(|T |·2|T ′ | ) whether T ∪ T ′ is a conservative extension of T , for some polynomial p().

A 2-EXPTIME lower bound was also established in [Ghilardi et al., 2006], thus the upper bound stated in Theorem 17 is tight. This lower bound transfers to the existence of uniform interpolants: one can show that T ′ = T ∪ {⊤ ⊑ C} is a conservative extension of T iff there is a uniform sig(T ) ∪ {r}-interpolant of

with r, A are fresh. This yields the main result of this section.

Theorem 18. It is 2-EXPTIME-complete to decide, given a TBox T and a signature Σ ⊆ sig(T ), whether there exists a uniform Σ-interpolant of T .

5 Computing Interpolants / Interpolant Size

We show how to compute smaller uniform interpolants than the non-elementary TΣ,M2 T +1 and establish a matching upper bound on their size. Let C be a concept and Σ ⊆ sig(C ) a signature. A concept C ′ is called a concept uniform Σinterpolant of C if sig(C ) ⊆ Σ, ∅ |= C ⊑ C ′ , and ∅ |= C ′ ⊑ D for every concept D such that sig(D) ⊆ Σ and ∅ |= C ⊑ D. The following result is proved in [ten Cate et al., 2006].

Theorem19. For every concept C and signatureΣ ⊆ sig(C ) one can effectively compute a concept uniform Σ-interpolant C ′ of C of at most exponential size in C.

This result can be lifted to (TBox) uniform interpolants by 'internalization' of the TBox. This is very similar to what is attempted in [Wang et al., 2010], but we use different bounds on the role depth of the internalization concepts. More specifically, let T = {⊤ ⊑ CT } have a uniform Σ-interpolant and R denote the set of role names in T . For a concept C, define inductively

It can be shown using Theorem 12 that for m = 22|CT |+1 + 2|CT | + 2 and C a concept uniform Σ-interpolant of ∀R≤m.CT , the TBox T ′ = {⊤ ⊑ C} is a uniform Σinterpolant of T . A close inspection of the construction underlying the proof of Theorem 19 applied to ∀R≤m.CT reveals that rd(C ) ≤ rd(∀R≤m.CT ) and that the size of C is at most triple exponential in |T |. This yields the following upper bound.

Theorem 20. Let T be an ALC-TBox and Σ ⊆ sig(T ). If there is a uniform Σ-interpolant of T , then there is one of size at most 222p(|T |) , p a polynomial.

A matching lower bound on the size of uniform interpolants can be obtained by transferring a lower bound on the size of so-called witness concepts for (non-)conservative extensions established in [Ghilardi et al., 2006]:

Theorem 21. There exists a signature Σ of cardinality 4 and a family of TBoxes (Tn)n>0 such that, for all n > 0,

• (i) |Tn| ∈ O(n2 ) and
• (ii) every uniform Σ-interpolant {⊤ ⊑ CT } for Tn is of size at least 2(2n ·22n )-2 .

6 Conclusions

We view the characterizations, tools, and results obtained in this paper as a general foundation for working with uniform interpolants in expressive DLs. In fact, we believe that the established framework can be extended to other expressive DLs such as ALC extended with number restrictions and/or inverse roles without too many hassles: the main modifications required should be a suitable modification of the notion of bisimulation and (at least in the case of number restrictions) a corresponding extension of the automata model. Other extensions, such as with nominals, require more efforts.

In concrete applications, what to do when the desired uniform Σ-interpolant does not exist? In applications such as ontology re-use and ontology summary, one option is to extend the signature Σ, preferably in a minimal way, and then to use the interpolant for the extended signature. We believe that Theorem 9 can be helpful to investigate this further, loosely in the spirit of Example 11. In applications such as predicate hiding, an extension of Σ might not be acceptable. It is then possible to resort to a more expressive DL in which uniform interpolants always exist. In fact, Theorem 15 and the fact that APTAs have the same expressive power as the μcalculus [Wilke, 2001] point the way towards the extension of ALC with fixpoint operators.

Acknowledgments.

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