Forgetting and Uniform Interpolation in Large-Scale Description Logic Terminologies

1 Introduction

The main application of ontologies in computer science is to fix the vocabulary of an application domain and to provide a formal theory that defines the meaning of terms built from the vocabulary and their relationships. Current applications lead to the development of very large and comprehensive ontologies such as the medical ontology SNOMED CT (Systematised Nomenclature of Medicine Clinical Terms) [Spackman, 2000] containing about 380 000 concept definitions and the National Cancer Institute ontology (NCI) [Sioutos et al., 2006] containing more than 60000 axioms. For ontologies T of this size, it is often of interest to forget a subvocabulary Σ of the vocabulary of T ; i.e., to transform T into a new ontology TΣ (called a Σ-interpolant of T ) that contains no symbols from Σ and that is indistinguishable from T regarding its consequences that do not use Σ. In AI, this problem has been studied under a variety of names such as forgetting and variable elimination [Reiter and Lin, 1994; Eiter and Wang, 2008; Lang et al., 2003]. In mathematical logic, this problem has been investigated as the uniform interpolation problem [Visser, 1996]. Computing Σ-interpolants of ontologies has a number of potential applications, e.g.,

Re-use of ontologies: when using ontologies such as SNOMED CT in an application, often only a very small fraction of its vocabulary is of interest. In this case, one could use a Σ-interpolant instead of the whole ontology, where Σ is the vocabulary not of interest for the application.

∗The research was supported by EPSRC grant EP/E065279/1.

Predicate hiding: an ontology developer might not want to publish an ontology completely because a certain part of its vocabulary is not intended for public use. Again, publishing Σ-interpolants, where Σ is the vocabulary to be hidden, appears to be a solution to this problem.

Exhibiting hidden relations between terms: large ontologies are difficult to maintain as small changes to its axioms can have drastic and damaging effects. To analyze possibly unwanted consequences over a certain part Γ of the vocabulary, an ontology developer can automatically generate a complete axiomatization of the relations between terms over Γ by computing a Σ-interpolant, where Σ is the complement of Γ.

Ontology versioning: to check whether two versions of an ontology have the same consequences over their common vocabulary (or a subset thereof), one can first compute their interpolants by forgetting the vocabulary not shared by the two versions and then check whether the two interpolants are logically equivalent (i.e., have the same models).

In the description of Σ-interpolants given above, we have neither specified a language in which they are axiomatized nor did we specify the language wrt. which Σ-interpolants should be indistinguishable from the original ontology. The choice of the latter language depends on the application: for example, if one is interested in inclusions between concepts, then a Σ-interpolant should imply the same concept inclusions using no symbols from Σ as the original ontology. On the other hand, if the ontology is used to query instance data using conjunctive queries, then a Σ-interpolant together with any instance data using no symbols from Σ should imply the same certain answers to conjunctive queries using no symbols from Σ as the original ontology.

Regarding the language L in which Σ-interpolants should be axiomatized, one has to find a compromise between the following three conflicting goals:

(R) Standard reasoning problems (e.g., logical equivalence) in L should not be more complex than reasoning in the language underlying the ontology.

(I) Σ-interpolants in L should be uniquely determined up to logical equivalence: if T ′ 1 and T ′ 2 are Σ-interpolants in L of ontologies T1 and T2 that have the same consequences not using Σ, then T ′ 1 and T ′ 2 should be logically equivalent.

(E) The language L should be powerful enough to admit finite and succinct (ideally, polynomial size) axiomatizations of Σ-interpolants, and it should be possible to compute Σinterpolants efficiently (ideally, in polynomial time).

For ontologies given in standard description logics (DLs) such as EL and any language between ALC and SHIQO, there do not exist languages L achieving all these goals simultaneously. 1 To illustrate this point, let L be second-order logic. Then L trivially satisfies (E) but fails to satisfy (R) and (I), for ontologies in any standard DL.

In this paper, we consider forgetting in the lightweight description logic EL underlying the designated OWL2-EL profile of the upcoming OWL Version 2 extended with role inclusions and domain and range restrictions [Baader et al., 2008]. This choice it motivated by the fact that forgetting appears to be of particular interest for large-scale and comprehensive ontologies and that many such ontologies are given in this language. We introduce three DLs for axiomatizing Σ-interpolants satisfying criteria (R) and (I) and preserving, respectively, inclusions between concepts, concept instances, and answers to conjunctive queries. These DLs do not satisfy (E), as Σ-interpolants sometimes to not exist or are of exponential size. We demonstrate that, nevertheless, Σ-interpolants typically exist and can be computed in practice for large-scale terminologies such as SNOMED CT and appropriate versions of NCI. Detailed proofs and additional experiments are available in a technical report [Konev et al., 2009].

2 Preliminaries

Let NC, NR, and NI be countably infinite and mutually disjoint sets of concept names, role names, and individual names. ELconcepts C are built according to the rule

where A ∈ NC, r ∈ NR, and C,D range over EL-concepts. The set of ELHr -inclusions consists of concept inclusions C ⊑ D and concept equations C ≡ D, domain restrictions dom(r) ⊑ C, range restrictions ran(r) ⊑ C and role inclusions r ⊑ s, where C,D are EL-concepts and r, s ∈ NR. An ELHr -TBox T is a finite set of ELHr -inclusions. An ELHr -TBox is called ELHr -terminology if all its concept inclusions and equations are of the form A ⊑ C and A ≡ C and no concept name occurs more than once on the left hand side. In what follows we use A ▷◁ C to denote expressions of the form A ⊑ C and A ≡ C.

Assertions of the form A(a) and r(a, b), where a, b ∈ NI, A ∈ NC, and r ∈ NR, are called ABox-assertions. An ABox is a finite set of ABox-assertions. By obj(A) we denote the set of individual names in A. A knowledge base (KB) is a pair (T ,A) consisting of a TBox T and an ABox A. Assertions of the form C(a) and r(a, b), where a, b ∈ NI, C a EL-concept, and r ∈ NR, are called instance assertions. To define the semantics of DLs considered in this paper we make use of the fact that DL-expressions can be regarded as formulas in FO, where FO denotes the set of first-order predicate logic formulas with equality using unary predicates in NC, binary predicates in NR, and constants from NI; see Figure 1 (in which the DL-constructors not considered so far are defined later). In what follows, we will not distinguish between DL-expressions and their translation into FO and regard TBoxes, ABoxes and KBs as finite subsets of FO. Thus, we use T |= ϕ to denote that ϕ follows from T in first-order logic even if ϕ is an ELHr -inclusion and T a subset of FO and similar conventions apply to DLs introduced later in this paper. FO (and, therefore, ELHr ) is interpreted in models I = (ΔI , ·I ), where the domain ΔI is a non-empty set, and ·I is a function mapping each concept name A to a subset AI of ΔI , each role name r to a binary relation rI ⊆ ΔI ×ΔI , and each individual name a to an element aI ∈ ΔI .

1 This follows from the fact that deciding whether TBoxes in these DLs imply the same concept inclusions over a signature is by at least one exponential harder than deciding logical equivalence [Lutz and Wolter, 2009; Lutz et al., 2007].

The most important ways of querying ELHr -TBoxes and KBs are subsumption (check whether T |= α for an ELHr - inclusion α), instance checking (check whether (T ,A) |= α for an instance assertion α), and conjunctive query answering. To define the latter, call a first-order formula q(⃗x) a conjunctive query if it is of the form ∃⃗yψ(⃗x, ⃗y), where ψ is a conjunction of expressions A(t) and r(t1, t2) with t, t1, t2 drawn from NI and sequences of variables ⃗x and ⃗y. If ⃗x has length k, then a sequence ⃗a of elements of obj(A) of length k is called a certain answer to q(⃗x) of a KB (T ,A) if (T ,A) |= q(⃗a).

3 Forgetting

A signature Σ is a subset of NC ∪ NR 2 . Given a signature Σ, we set Σ = (NC ∪ NR) \ Σ. Given a concept, role, concept inclusion, TBox, ABox, FO-sentence, set of FOsentences E, we denote by sig(E) the signature of E, that is, the set of concept and role names occurring in it. We use the term ELHrΣ-inclusion (Σ-ABox, Σ-query, LΣ-sentence, etc.) to denote ELHr -inclusions (ABoxes, queries, L-sentences, etc.) whose signature is contained in Σ.

To define forgetting, we first formalize the notion of inseparability between TBoxes wrt. a signature. Intuitively, two TBoxes T1 and T2 are inseparable wrt. a signature Σ if they have the same Σ-consequences, where the set of Σ-consequences considered can either reflect subsumption queries, instance queries, or conjunctive queries, depending on the application. We give the definitions for sets of FOsentences because we later require these notions for a variety of DLs.

2 We investigate forgetting for TBoxes for DLs without nominals; thus we do not include individual names into the signature.

Definition 1. Let T1 and T2 be sets of FO-sentences and Σ a signature.

-T1 and T2 are concept Σ-inseparable, in symbols T1 ≡CΣ T2, if for all ELHrΣ-inclusions α: T1 |= α⇔ T2 |= α.

-T1 and T2 are instance Σ-inseparable, in symbols T1 ≡iΣ T2, if for all Σ-ABoxes A and Σ-instance assertions α using individual names from obj(A): (T1, A) |= α ⇔ (T2, A) |= α. -T1 and T2 are query Σ-inseparable, in symbols T1 ≡qΣ T2, if for all Σ-ABoxes A, conjunctive Σ-queries q(⃗x), and vectors ⃗a of the same length as ⃗x of individual names in obj(A): (T1, A) |= q(⃗a) ⇔ (T2, A) |= q(⃗a).

The definition of forgetting (Σ-interpolants) is now straightforward.

Definition 2 (Σ-interpolant). Let T be an ELHr -TBox, Σ a finite signature, and L a set of FO-sentences. If TΣ is a finite set of LΣ-sentences such that T |= ϕ for all ϕ ∈ TΣ, then TΣ is

• a concept Σ-interpolant of T in L if T ≡CΣ TΣ;
• an instance Σ-interpolant of T in L if T ≡iΣ TΣ;
• a query Σ-interpolant of T in L if T ≡qΣ TΣ.

One can show that every query Σ-interpolant is an instance Σ-interpolant and every instance Σ-interpolant is a concept Σ-interpolant. The converse implications do not hold, even for ELHr -terminologies:

Example 3. Let T = {ran(r) ⊑ A1, ran(s) ⊑ A2,B ≡ A1 ⊓ A2} and Σ = {A1,A2}. One can show that the empty TBox is a concept Σ-interpolant of T . However, the empty TBox is not an instance Σ-interpolant of T . To show this, consider the Σ-ABox A = {r(a0, b), s(a1, b)}. Then (T ,A) |= B(b) but (∅,A) ̸|= B(b). Observe that no ELHr -TBox (and even no SHQ-TBox) is an instance Σ-interpolant of T because it is impossible to capture the ABox A in a DL in which one cannot refer to the range of distinct roles in one concept. On the other hand, the TBox T ′ = {ran(r) ⊓ ran(s) ⊑ B} given in an extension of ELHr is an instance Σ-interpolant of T .

Example 4. Let T = {A ⊑ ∃s.⊤, s ⊑ r1, s ⊑ r2} and Σ = {s}. Then T ′ = {A ⊑ ∃r1.⊤ ⊓ ∃r2.⊤} is an instance Σ-interpolant of T , but T ′ is not a query Σ-interpolant of T . To show the latter, let A = {A(a)} and let q = ∃x(r1(a, x)∧ r2(a, x)). Then (T ,A) |= q but (T ′ ,A) ̸|= q. Again, no ELHr -TBox (and even no TBox in SHIQ) is a query Σinterpolant of T . On the other hand, the TBox T ′′ = {A ⊑ ∃r1⊓r2.⊤} given in an extension of ELHr with conjunctions of roles names is a query Σ-interpolant of T .

Besides of exhibiting examples where concept, instance, and query Σ-interpolants are distinct, Example 3 and 4 also show that even in extremely simple cases ELHr and a variety of more expressive DLs are not sufficiently powerful to express instance and query Σ-interpolants of ELHr -terminologies. Rather surprisingly, there also exist simple examples in which ELHr -TBoxes are not sufficiently expressive to axiomatize concept Σ-interpolants of ELHr -terminologies.

Example 5. Let Σ = {Research Inst, Education Inst} and

T be University ≡ Research Inst ⊓ Education Inst School ⊑ Education Inst

ran(PhD from) ⊑ Research Inst

Then there does not exist an ELHr -TBox that is a concept Σ-interpolant of T . Intuitively, the reason is that there is no ELHrΣ-TBox which follows from T and has the following infinite set of Σ-consequences (which are consequences of T ):

∃PhD from.(School ⊓ A) ⊑ ∃PhD from.(University ⊓ A), where A ∈ Σ. On the other hand, the TBox T ′ = {ran(PhD from) ⊓ School ⊑ University} given in an extension of ELHr is a concept Σ-interpolant of T .

We now introduce three extensions of ELHr which we propose to axiomatize concept, instance, and query Σinterpolants.

Definition 6 (ELran,0 , ELran , ELran,⊓,u ). C ran,0 -concepts are constructed using the following syntax rule

where D ranges over EL-concepts and r ∈ NR. The set of ELran,0 -inclusions consists of concept inclusions C ⊑ D and role inclusions r ⊑ s, where C is a C ran,0 -concept, D an ELconcept, and r, s ∈ NR.

C ran -concepts are constructed using the following syntax

rule C := A | ran(r) | C ⊓D | ∃r.C, where A ∈ NC, C,D range over C ran -concepts and r ∈ NR. The set of ELran -inclusions consists of all concept inclusions C ⊑ D and role inclusions r ⊑ s, where C is a C ran -concept, D an EL-concept, and r, s ∈ NR.

Let u (the universal role) be a fresh logical symbol. C ⊓,u - concepts are constructed using the following syntax rule

C := A | C ⊓D | ∃R.C | ∃u.C, where A ∈ NC, C,D range over C ⊓,u -concepts and R = r1 ⊓ · · · ⊓ rn with r1, . . . , rn ∈ NR. The set of ELran,⊓,u - inclusions consists of concept inclusions C ⊑ D and role inclusions r ⊑ s, where C is a C ran -concept, D a C ⊓,u -concept, and r, s ∈ NR.

An X-TBox is a finite set of X-inclusions, where X ranges over ELran , ELran,0 , and ELran,⊓,u .

We have the following inclusions:

where L1 ◁ L2 means that every L1-TBox is logically equivalent to some L2-TBox. The semantics of the additional constructors is straightforward and given in Figure 1. We regard the universal role u as a logical symbol (i.e., u ̸∈ NR). This interpretation reflects the fact that the signature of the firstorder translation of ∃u.C coincides with the signature of C. Observe that the TBox given as a concept Σ-interpolant in Example 5 is an ELran,0 -TBox; the instance Σ-interpolant given in Example 3 is an ELran -TBox, and the query Σinterpolant in Example 4 is an ELran,⊓,u -TBox. For an example illustrating the need of the universal role for query Σinterpolants, see [Lutz and Wolter, 2009].

We show that the languages introduced in Definition 6 satisfy criteria (R) and (I) from the introduction. (R) is a consequence of the following result.

Theorem 7. The following problems are PTIME-complete for ELran,⊓,u -TBoxes T and ABoxes A: decide whether

• T |= C ⊑D, for C ⊑D an ELran,⊓,u -inclusion;
• (T ,A) |= C(a), where C is an EL-concept.

Deciding whether (T ,A) |= q(⃗a), where q is a conjunctive query, is NP-complete, and deciding this problem for fixed q(⃗a) (knowledge base complexity) is PTIME-complete.

It follows, in particular, that logical equivalence of ELran,⊓,u - TBoxes is decidable in PTime. These complexity results are exactly the same as for ELH-TBoxes [Rosati, 2007]. For (I) and the computation of Σ-interpolants below, we first investigate the relationship between the distinct inseparability notions introduced in Definition 1 and inseparability wrt. the new languages. (For EL this relationship is characterized in [Lutz and Wolter, 2009].) Let X range over the superscripts ran, 0 and ran and ran, ⊓, u. Say that two finite sets of FO-sentences T1 and T2 are X-inseparable wrt. Σ, in symbols T1 ≡XΣ T2, if T1 |= α ⇔ T2 |= α, for all ELXΣ -inclusions α.

Theorem 8. Let T1 and T2 be ELran,⊓,u -TBoxes and Σ an infinite signature. Then the following holds:

• T1 ≡CΣ T2 iff T1 ≡ran,0 Σ T2;
• T1 ≡iΣ T2 iff T1 ≡ran Σ T2;
• T1 ≡qΣ T2 iff T1 ≡ran,⊓,u Σ T2.

The condition that Σ is infinite is required only for the implication from right to left in Point 1. As we forget finite signatures, their complement is always infinite.

From Theorem 8 we immediately obtain that (I) is met for the three notions of Σ-interpolants. For example, assume that T1 and T2 are ELHr -TBoxes such that T1 ≡qΣ T2 and let T ′ 1 and T ′ 2 be query Σ-interpolants in ELran,⊓,u of T1 and T2, respectively. By Theorem 8, T ′ 1 ≡ran,⊓,u Σ T ′ 2 . But then T ′ 1 and T ′ 2 are logically equivalent: we have T ′ 1 |= α for all α ∈ T ′ 2 because all such α are ELran,⊓,u Σ -inclusions and T ′ 2 |= α. The converse direction holds for the same reason.

4 Computing Σ-interpolants

We give a recursive algorithm computing instance Σinterpolants for ELHr -terminologies satisfying certain acyclicity conditions (similar algorithms computing concept and query Σ-interpolants are given in the technical report [Konev et al., 2009]). In this section we assume wlog. that terminologies are normalized ELHr terminologies; i.e., ELHr -terminologies T consisting of role inclusions and axioms of the form (here, and in what follows, we write r ⊑T s if T |= r ⊑ s)

• A ▷◁ ∃r.B, where B ∈ NC ∪ {⊤};
• A ▷◁ B1 ⊓ · · · Bn, where B1, . . . , Bn ∈ NC;
• dom(s) ⊑ A and ran(s) ⊑ A, where A ∈ NC

such that dom(s) ⊑ A ∈ T and r ⊑T s imply dom(r) ⊑ A ∈ T ; ran(s) ⊑ A ∈ T and r ⊑T s imply ran(r) ⊑ A ∈ T ; and r ⊑T s and s ⊑T r implies r = s. We give the acyclicity conditions required for the algorithms to terminate. The Σ-cover C Σ T (r) of a role r wrt. a terminology T consists of all s ∈ Σ such that r ⊑T s and there does not exist r′ ∈ Σ with r′ ̸= s and r ⊑T r′ ⊑T s.

Definition 9 (Σ-loop). Let T be a normalized ELHr - terminology and Σ a signature. Define a relation ≺Σ⊆ (NC ∩

• Σ) × (NC ∩ Σ) as follows: A ≺Σ B if A, B ∈ Σ and

• (b) A ▷◁ ∃r.A′ ∈ T for some A′ ∈ NC ∪{⊤} and r ∈ Σ such that dom(r) ⊑ B ∈ T , or
• (c) A ▷◁ ∃r.A′ ∈ T for some A′ ∈ NC ∪ {⊤} and r such that there exists s ∈ C Σ T (r) with ran(r) ⊑ B ∈ T , ran(s) ⊑ B ̸∈ T .

We say that T contains a Σ-loop if ≺Σ contains a cycle.

The following example illustrates this definition and shows that the existence of Σ-loops typically entails the nonexistence of Σ-interpolants, even in FO.

Example 10. Consider the set of inclusions

and define ELHr -terminologies T1 = {(1), (2)}, T2 = {(1), (3), (4)}, and T3 = {(1), (3), (5), (6)}, and let Σi = sig(Ti) \ {Elephant, has mother}, for i = 1, 2, 3. Even in FO, there exists no concept/instance/query Σi-interpolant of Ti. To see this observe that in all three cases an infinite axiomatization of such a Σ-interpolant is given by the inclusions

This theory cannot be finitely axiomatized in FO without additional predicates. Observe that T1 contains a Σ1-loop as axiom (2) implies Mammal ≺Σ1 Mammal by clause (a) of Definition 9 for Σ1-loops; T2 contains a Σ′2 -loop as axioms (3) and (4) imply Mammal ≺Σ′2 A ≺Σ′2 Mammal by clauses (a) and (b), where the fresh concept name A is due to normalization introducing

dom(has mam′ l father) ⊑ A, A ⊑ ∃has mother.Mammal;

and T3 contains a Σ3-loop as axioms (3), (5), and (6) imply Mammal ≺Σ3 Mammal by clause (c).

Call a concept name A primitive (pseudo-primitive) in a terminology T if A does not occur on the left hand side of any axiom in T (does not occur in the form A ≡ C in T ).

The intuition behind the following algorithm for Σinterpolants is as follows: first, one can show using Theorem 8 and a sequent-style proof system for ELHr that under the conditions of Theorem 11 there exists an instance Σinterpolant consisting of (in addition to role inclusions and domain and range restrictions) concept inclusions of the form C ⊑ A and A ⊑ C. In Figure 2, we compute the set PΣ(A) of Cs such that C ⊑ A is in the interpolant by making a case distinction: in Point 1 A is pseudo-primitive; in Point 2 it is defined by a conjunction; in Point 3 it is defined as ∃r.A′ . Points 2 and 3 are recursive as they require the sets PΣ(B)

For A ∈ sig(T ), let PreΣ(A) consist of all D = ran(r), D = ∃r.⊤, andD ∈ NC such that T |=D ⊑ Aand sig(D) ⊆ sig(T )∩ Σ; construct PΣ(A) as follows:

• for A pseudo-primitive in T , PΣ(A) = PreΣ(A);
• if A ≡ B1 ⊓ · · · ⊓Bn ∈ T , then PΣ(A) = {CB1 ⊓ · · · ⊓CBn | (Bi ∈ Σ and CBi = Bi) or (Bi ∈ Σ and CBi ∈ PΣ(Bi))};
• if A ≡ ∃r.A′ ∈ T , then PΣ(A) is the union of PreΣ(A) and
• if A′ ∈ Σ: {∃s.A′ | s ⊑T r, s ∈ Σ};
• if A′ ̸∈ Σ: {∃s.D | s ⊑T r, s ∈ Σ,D′ ∈ PΣ(A′ )}.

Figure 2: Computing PΣ(A)

For A ∈ sig(T ), let PostΣ(A) = {B ∈ Σ∩ sig(T ) | T |= A ⊑ B} and construct QΣ(A) as follows:

• for A primitive in T , QΣ(A) = PostΣ(A);
• if A ▷◁ B1 ⊓ · · · ⊓Bn ∈ T , then QΣ(Bi);

• if A ▷◁ ∃r.A′ ∈ T , then QΣ(A) is the union of PostΣ(A),

[

r⊑T s{QΣ(B) | dom(s) ⊑ B ∈ T , s ∈ Σ, B ∈ Σ},

and

where

Figure 3: Computing QΣ(A)

when B is used in the definition of A. Σ-loops describe exactly the situation in which the recursion does not terminate. In Figure 3 we compute, in a similar way, the set QΣ(A) of Cs such that A ⊑ C is in the interpolant. A sample run of the algorithm is provided in [Konev et al., 2009].

Theorem11. Let Σ be a finite signature and T a normalized ELHr -terminology without Σ-loops. Then the algorithms computing PΣ(A) and QΣ(A) in Figures 2 and 3 terminate for all A ∈ sig(T ).

Let TΣ consist of the following inclusions, where A, r, and s range over sig(T ) ∩ Σ:

• r ⊑ s, for r ⊑T s;
• D ⊑ A, for all D ∈ PΣ(A);
• A ⊑D, for all D ∈ QΣ(A);
• ran(r) ⊑ D, for all D ∈ QΣ(B) such that ran(r) ⊑ B ∈ T and B ∈ Σ;
• dom(r) ⊑ D, for all D ∈ QΣ(B) such that dom(r) ⊑ B ∈ T and B ∈ Σ;

Then TΣ is an instance Σ-interpolant of T .

PΣ(A) and QΣ(A) are both of exponential size, in the worst case. For PΣ(A), this is clear from Point 2 of the construction: let T consist of A ≡ B1 ⊓ · · · ⊓ Bn and Aji ⊑ Bi (1 ≤ i, j ≤ n) and let Σ = {Bi | 1 ≤ i ≤ n}. Then PΣ(A) is of size nn , and one can show that there does not exist a shorter Σ-interpolant in ELran,⊓,u . For QΣ(A) this follows from the fact that one might have to construct a complete unfolding of the terminology.

If we admit disjunctions in C in axioms C ⊑ D of Σinterpolants, then we can replace, in Point 2, PΣ(A) for A ≡ B1 ⊓ · · · ⊓ Bn ∈ T by the singleton set consisting of

We will see below that in practice this construction leads to much smaller Σ-interpolants. However, this improvement does not come for free. Consider the language ELran,⊔, where the only difference to ELran is that C ran -concepts now admit '⊔' as a binary concept constructor. Every ELran,⊔-TBox is logically equivalent to an (exponentially larger) ELran -TBox, and so ELran,⊔ inherits many desirable properties from ELran . However, one can show that, in contrast to ELran , logical equivalence between ELran,⊔-TBoxes is coNP-hard.

5 Experiments

We have implemented a prototype called NUI that computes instance Σ-interpolants as presented in Theorem 11. We have applied NUI to a version of SNOMED CT dated 09 February 2005 (without two left-identities) and the ELHr -fragment of the release 08.08d of NCI. The first terminology has approx. 380K axioms, almost the same number of concept names, and 56 role names. The ELHr -fragment of NCI has approx. 63K axioms, approx. 65K concept names, and 123 role names. We note that the algorithms given above compute (for ease of exposition) a large number of redundant axioms and NUI implements a variety of straightforward optimizations.

First observe that neither SNOMED CT nor NCI contain any Σ-loops, for any signature Σ. Thus, Σ-interpolants always exist and can, in principle, be computed using our algorithm.

In our experiments, we focus on the case of forgetting a large signature Σ (and keeping a "small" signature Σ∩sig(·)), as this corresponds to many application scenarios. The experiments have been performed on a standard PC with 2.13 GHz and 3 GB of RAM.

Success rate: Table 1 shows the rate at which NUI succeeds to compute instance Σ-interpolants of SNOMED CT and NCI wrt. various signatures. All failed cases are due to memory overflow after several hours. For each table entry, 100 samples have been used. The signatures contain concept and role names randomly selected from the full signature of SNOMED CT (we never forget the role 'roleGroup' as this would make forgetting trivial) and NCI, respectively. Σ ∩ sig(·) always contains 20 role names. For NCI and signatures of size ≤ 4 000, NUI had a 100% success rate.

Size: We compare the size of instance Σ-interpolants of SNOMED CT and NCI computed by NUI with the size of extracted Σ∩ sig(·)-modules; i.e., minimal subsetsMof the respective terminologies which preserve, e.g., inclusions between Σ ∩ sig(·)-concepts. We use MEX-modules [Konev et al., 2008a] of SNOMED CT and ⊤-local modules [Cuenca Grau et al., 2007] of NCI. The size of Σ-interpolants, terminologies, and modules is measured as number of symbols rather than number of axioms as Σ-interpolants can contain large axioms.

For SNOMED CT, we computed instance Σ-interpolants and Σ∩sig(·)-modules wrt. 100 random signatures with 3 000 concept names and 20 role names in Σ ∩ sig(·). 48.19% of instance Σ-interpolants are smaller than the corresponding modules, whose sizes lie between 2.94% and 3.21% of SNOMEDCT. However, the largest instance Σ-interpolant is more than 11 times larger than SNOMED CT.

For NCI, we computed instance Σ-interpolants and Σ ∩ sig(·)-modules wrt. 100 random signatures with 7000 concept names and 20 role names in Σ ∩ sig(·). 74.47% of the instance Σ-interpolants are smaller than the corresponding modules, whose sizes lie between 21.62% and 23.17% of NCI. NUI computes each of those interpolants within 25 min. However, the largest instance Σ-interpolant is more than 12 times larger than NCI.

Forgetting with disjunction: All failures in Table 1 are due to the fact that PΣ(A) is too large. Indeed, if we admit disjunction and consider ELran,⊔, then NUI succeeds to compute all Σ-interpolants from Table 1, each within 15 min. Moreover, for NCI, no signature for which NUI fails has been detected. For SNOMED CT, however, NUI still typically fails for |Σ ∩ sig(·)| ≥ 30 000.

6 Discussion

The notion of forgetting in DL ontologies has recently been investigated in a number of research papers. [Kontchakov et al., 2008; Wang et al., 2008] consider forgetting in DL-Lite and [Eiter et al., 2006] investigate in how far forgetting in DLs can be reduced to forgetting in logic programs. [Konev et al., 2008b], on which this paper is based, proposes forgetting for acyclic EL-terminologies and concept inclusions.

The main novel contributions of this paper are (i) the first algorithms with experimental results indicating the practical feasibility of forgetting in DL-terminologies and (ii) the first systematic analysis of the distinct languages required to axiomatize Σ-interpolants for distinct queries languages. Many open problems remain; e.g., we conjuncture that Σ-interpolants of ELHr -terminologies (and possibly even TBoxes) exist in the languages introduced whenever they exist in FO. Such a result would provide further justification for those languages. Secondly, it would be of interest to prove decidability (and complexity) of the decision problem whether there exists a Σ-interpolant for a given ELHr -terminology (TBox). Note that our acyclicity conditions are sufficient but not necessary for the existence of Σinterpolants.