=Paper=
{{Paper
|id=Vol-477/paper-19
|storemode=property
|title=Forgetting and uniform interpolation in extensions of the description logic EL
|pdfUrl=https://ceur-ws.org/Vol-477/paper_28.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/KonevWW09
}}
==Forgetting and uniform interpolation in extensions of the description logic EL==
https://ceur-ws.org/Vol-477/paper_28.pdf
Forgetting and uniform interpolation in extensions of
the description logic EL
Boris Konev, Dirk Walther, and Frank Wolter?
University of Liverpool, UK
{konev, dwalther, wolter}@liverpool.ac.uk
1 Introduction
Terminologies used in life sciences, health-care, and other knowledge intensive ar-
eas are often very large and comprehensive. Examples are the medical terminology
SNOMED CT (Systematised Nomenclature of Medicine Clinical Terms) [17] con-
taining about 380 000 concept definitions and the National Cancer Institute ontology
(NCI) [16] containing more than 60 000 axioms. For terminologies 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 terminology 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 vari-
able elimination [14, 4, 10]. In mathematical logic, this problem has been investigated
as the uniform interpolation problem [18]. Computing Σ-interpolants of terminologies
has a number of potential applications, e.g.,
Re-use of ontologies: when using terminologies 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 terminology, where Σ is the vocabulary not of
interest for the application.
Predicate hiding: a terminology developer might not want to publish a terminology
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 terminologies are difficult to maintain
as small changes to its axioms can have drastic and damaging effects. To analyze pos-
sibly unwanted consequences over a certain part Γ of the vocabulary, an ontology de-
veloper 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 a terminology 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 lan-
guage in which they are axiomatized nor did we specify the language wrt. which Σ-
interpolants should be indistinguishable from the original termininology. The choice of
?
This research was supported by the EPSRC grant EP/E065279/1.
the latter language depends on the application: for example, if one is interested in inclu-
sions between concepts, then a Σ-interpolant should imply the same concept inclusions
using no symbols from Σ as the original terminology. On the other hand, if the termi-
nology 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 terminology.
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 terminology.
(I) Σ-interpolants in L should be uniquely determined up to logical equivalence: if T10
and T20 are Σ-interpolants in L of terminologies T1 and T2 that have the same conse-
quences not using Σ, then T10 and T20 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 com-
pute Σ-interpolants efficiently (ideally, in polynomial time).
For terminologies 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 under-
lying the designated OWL2-EL profile of the upcoming OWL Version 2 extended with
role inclusions and domain and range restrictions [1]. This choice it motivated by the
fact that forgetting appears to be of particular interest for large-scale and comprehen-
sive terminologies and that many such terminologies 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 do
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. This work has been presented in [7];
detailed proofs and additional experiments are available in a technical report [8].
2 Preliminaries
Let NC , NR , and NI be countably infinite and mutually disjoint sets of concept names,
role names, and individual names. EL-concepts C are built according to the rule
C := A | > | C uD | ∃r.C,
where A ∈ NC , r ∈ NR , and C, D range over EL-concepts. The set of ELHr -inclusions
consists of concept inclusions C v D and concept equations C ≡ D, domain restric-
tions dom(r) v C, range restrictions ran(r) v C and role inclusions r v s, where
1
This follows from the fact that deciding whether TBoxes in these DLs imply the same concept
inclusions over a signature is at least one exponential harder than deciding logical equiva-
lence [12, 11].
Concept C Translation C ] Concept C Translation C ]
> x=x dom(r) ∃y (r(x, y))
A A(x) ran(r) ∃y (r(y, x))
C uD C ] (x) ∧ D] (x) ∃u.C (x = x) ∧ ∃y C ] (y)
∃r.C ∃y (r(x, y) ∧ C ] (y)) ∃r1 u · · · u rn .C ∃y(r1 (x, y) ∧ · · · ∧ rn (x, y) ∧ C ] (y))
Fig. 1. Standard translation ·]
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 v 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 v 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 .
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 de-
fine 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
2
We investigate forgetting for TBoxes for DLs without nominals; thus we do not include indi-
vidual names into the signature.
FO-sentences 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 FO-sentences because we later
require these notions for a variety of DLs.
Definition 1. Let T1 and T2 be sets of FO-sentences and Σ a signature.
r
–T1 and T2 are concept Σ-inseparable, in symbols T1 ≡CΣ T2 , if for all ELHΣ -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
C
– a concept Σ-interpolant of T in L if T ≡Σ TΣ ;
i
– an instance Σ-interpolant of T in L if T ≡Σ 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 1. Let T = {ran(r) v A1 , ran(s) v A2 , B ≡ A1 u 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) 6|= 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 0 = {ran(r) u ran(s) v B}
given in an extension of ELHr is an instance Σ-interpolant of T .
Example 2. Let T = {A v ∃s.>, s v r1 , s v r2 } and Σ = {s}. Then T 0 = {A v
∃r1 .> u ∃r2 .>} is an instance Σ-interpolant of T , but T 0 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 0 , A) 6|= q. Again, no ELHr -TBox (and even no TBox in SHIQ) is
a query Σ-interpolant of T . On the other hand, the TBox T 00 = {A v ∃r1 ur2 .>} 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 1 and 2 also show that even in extremely simple cases ELHr and a va-
riety of more expressive DLs are not sufficiently powerful to express instance and query
Σ-interpolants of ELHr -terminologies. Rather surprisingly, there also exist simple ex-
amples in which ELHr -TBoxes are not sufficiently expressive to axiomatize concept
Σ-interpolants of ELHr -terminologies.
Example 3. Let Σ = {Research Inst, Education Inst} and T be
University ≡ Research Inst u Education Inst
School v Education Inst
ran(PhD from) v Research Inst
Then there does not exist an ELHr -TBox that is a concept Σ-interpolant of T . Intu-
r
itively, the reason is that there is no ELHΣ -TBox which follows from T and has the
following infinite set of Σ-consequences (which are consequences of T ):
∃PhD from.(School u A) v ∃PhD from.(University u A),
where A ∈ Σ. On the other hand, the TBox T 0 = {ran(PhD from) u School v
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 3 (ELran,0 , ELran , ELran,u,u ). C ran,0 -concepts are constructed using the fol-
lowing syntax rule
C := D | ran(r) | ran(r) u D,
where D ranges over EL-concepts and r ∈ NR . The set of ELran,0 -inclusions consists
of concept inclusions C v D and role inclusions r v s, where C is a C ran,0 -concept, D
an EL-concept, and r, s ∈ NR .
C ran -concepts are constructed using the following syntax rule
C := A | ran(r) | C u 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 v D and role inclusions r v 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,u -concepts are constructed
using the following syntax rule
C := A | C uD | ∃R.C | ∃u.C,
u,u
where A ∈ NC , C, D range over C -concepts and R = r1 u· · ·urn with r1 , . . . , rn ∈
NR . The set of ELran,u,u -inclusions consists of concept inclusions C v D and role
inclusions r v s, where C is a C ran -concept, D a C u,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,u .
We have the following inclusions:
ELHr C ELran,0 C ELran C ELran,u,u
where L1 C 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 6∈ NR ). This interpretation re-
flects the fact that the signature of the first-order translation of ∃u.C coincides with the
signature of C. Observe that the TBox given as a concept Σ-interpolant in Example 3
is an ELran,0 -TBox; the instance Σ-interpolant given in Example 1 is an ELran -TBox,
and the query Σ-interpolant in Example 2 is an ELran,u,u -TBox. The need for the uni-
versal role is illustrated by considering T = {A v ∃r.B} and Σ = {r}. The empty
TBox is a concept and an instance Σ-interpolant of T . A query Σ-interpolant is given
by T 0 = {A v ∃u.B} and reflects the fact that (T , A) |= ∃xB(x) for A = {A(a)}.
We show that the languages introduced in Definition 3 satisfy criteria (R) and (I)
from the introduction. (R) is a consequence of the following result.
Theorem 1. The following problems are PTIME-complete for ELran,u,u -TBoxes T and
ABoxes A: decide whether
– T |= C v D, for C v D an ELran,u,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,u -TBoxes is decidable in
PTime. These complexity results are exactly the same as for ELH-TBoxes [15]. For (I)
and the computation of Σ-interpolants below, we first investigate the relationship be-
tween the distinct inseparability notions introduced in Definition 1 and inseparability
wrt. the new languages. (For EL this relationship is characterized in [13].) Let X range
over the superscripts ‘ran, 0’, ‘ran’, and ‘ran, u, 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 2. Let T1 and T2 be ELran,u,u -TBoxes and Σ an infinite signature. Then the
following holds:
ran,0
– T 1 ≡C
Σ T2 iff T1 ≡Σ T2 ;
i ran
– T1 ≡Σ T2 iff T1 ≡Σ T2 ;
– T1 ≡qΣ T2 iff T1 ≡Σ
ran,u,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 2 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 T10 and T20 be query Σ-interpolants in ELran,u,u of T1 and T2 , respectively.
By Theorem 2, T10 ≡ran,u,u
Σ
T20 . But then T10 and T20 are logically equivalent: we have
0 0 ran,u,u
T1 |= α for all α ∈ T2 because all such α are ELΣ -inclusions and T20 |= α. The
converse direction holds for the same reason.
4 Computing Σ-interpolants
We give a recursive algorithm computing instance Σ-interpolants for ELHr -termino-
logies satisfying certain acyclicity conditions (similar algorithms computing concept
and query Σ-interpolants are presented in the technical report [8]). 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 vT s if T |= r v s)
– A ./ ∃r.B, where B ∈ NC ∪ {>};
– A ./ B1 u · · · Bn , where B1 , . . . , Bn ∈ NC ;
– dom(s) v A and ran(s) v A, where A ∈ NC
such that dom(s) v A ∈ T and r vT s imply dom(r) v A ∈ T ; ran(s) v A ∈ T and
r vT s imply ran(r) v A ∈ T ; and r vT s and s vT r implies r = s. We give the
acyclicity conditions required for the algorithms to terminate. The Σ-cover CTΣ (r) of a
role r wrt. a terminology T consists of all s ∈ Σ such that r vT s and there does not
exist r0 ∈ Σ with r0 6= s and r vT r0 vT s.
Definition 4 (Σ-loop). Let T be a normalized ELHr -terminology and Σ a signature.
Define a relation ≺Σ ⊆ (NC ∩ Σ) × (NC ∩ Σ) as follows: A ≺Σ B if A, B ∈ Σ and
(a) A ./ C ∈ T for some C such that B occurs in C, or
(b) A ./ ∃r.A0 ∈ T for some A0 ∈ NC ∪ {>} and r ∈ Σ such that dom(r) v B ∈ T ,
or
(c) A ./ ∃r.A0 ∈ T for some A0 ∈ NC ∪ {>} and r such that there exists s ∈ CTΣ (r)
with ran(r) v B ∈ T , ran(s) v B 6∈ 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 non-existence of Σ-interpolants, even in FO.
Example 4. Consider the terminology
T = {Elephant v Mammal, Mammal v ∃has mother.Mammal}
and let Σ = {Mammal}. Even in FO, there exists no concept/instance/query Σ-inter-
polant of T . To see this observe that an infinite axiomatization of such a Σ-interpolant
is given by the inclusions
n
z }| {
{Elephant v ∃has mother. · · · ∃has mother .> | n ≥ 1}.
This theory cannot be finitely axiomatized in FO without additional predicates. Observe
that T contains the Σ-loop as Mammal ≺Σ Mammal.
Examples illustrating the points (b) and (c) of Definition 4 of Σ-loops can be found in
the technical report [8].
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 ).
For A ∈ sig(T ), let PreΣ (A) consist of all D = ran(r), D = ∃r.>, and D ∈ NC such that
T |= D v A and sig(D) ⊆ sig(T ) ∩ Σ; construct PΣ (A) as follows:
1. for A pseudo-primitive in T , PΣ (A) = PreΣ (A);
2. if A ≡ B1 u · · · u Bn ∈ T , then
PΣ (A) = {CB1 u · · · u CBn | (Bi ∈ Σ and CBi = Bi )
or (Bi ∈ Σ and CBi ∈ PΣ (Bi ))};
3. if A ≡ ∃r.A0 ∈ T , then PΣ (A) is the union of PreΣ (A) and
– if A0 ∈ Σ: {∃s.A0 | s vT r, s ∈ Σ};
– if A0 6∈ Σ: {∃s.D | s vT r, s ∈ Σ, D ∈ PΣ (A0 )}.
Fig. 2. Computing PΣ (A)
For A ∈ sig(T ), let PostΣ (A) = {B ∈ Σ ∩ sig(T ) | T |= A v B} and construct QΣ (A) as
follows:
1. for A primitive in T , QΣ (A) = PostΣ (A);
2. if A ./ B1 u · · · u Bn ∈ T , then
[
QΣ (A) = PostΣ (A) ∪ QΣ (Bi );
1≤i≤n,Bi ∈Σ
3. if A ./ ∃r.A0 ∈ T , then QΣ (A) is the union of PostΣ (A) and
[
{∃s.Es | s ∈ CTΣ (r)} ∪ {QΣ (B) | dom(s) v B ∈ T , s ∈ Σ, B ∈ Σ},
rvT s
where l l l
Es = D u D u B.
B∈Σ, ran(r)vB∈T D∈QΣ (A0 ) B∈Σ
ran(s)vB6∈T, D∈QΣ (B) A0 ∈Σ T |=ran(r)uA0 vB
Fig. 3. Computing QΣ (A)
The intuition behind the following algorithm for Σ-interpolants is as follows: first,
one can show using Theorem 2 and a sequent-style proof system for ELHr that under
the conditions of Theorem 3 there exists an instance Σ-interpolant consisting of (in
addition to role inclusions and domain and range restrictions) concept inclusions of the
form C v A and A v C. In Figure 2, we compute the set PΣ (A) of Cs such that C v 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.A0 . Points 2 and 3 are
recursive as they require the sets PΣ (B) 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 v C is in the interpolant.
A sample run of the algorithm is provided in [8].
Theorem 3. Let Σ be a finite signature and T a normalized ELHr -terminology with-
out Σ-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 v s, for r vT s;
– D v A, for all D ∈ PΣ (A);
– A v D, for all D ∈ QΣ (A);
– ran(r) v D, for all D ∈ QΣ (B) such that ran(r) v B ∈ T and B ∈ Σ;
– dom(r) v D, for all D ∈ QΣ (B) such that dom(r) v 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 u · · · u Bn and Aji v 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,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 v D of Σ-interpolants, then we can
replace, in Point 2, PΣ (A) for A ≡ B1 u · · · u Bn ∈ T by the singleton set consisting
of l l G
Bi u CBi .
1≤i≤n,Bi ∈Σ 1≤i≤n,Bi ∈Σ CBi ∈PΣ (Bi )
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,t ,
where the only difference to ELran is that C ran -concepts now admit ‘t’ as a binary
concept constructor. Every ELran,t -TBox is logically equivalent to an (exponentially
larger) ELran -TBox, and so ELran,t inherits many desirable properties from ELran .
However, one can show that, in contrast to ELran , logical equivalence between ELran,t -
TBoxes is coNP-hard.
5 Experiments
We have implemented a prototype called NUI that computes instance Σ-interpolants
as presented in Theorem 3. 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 num-
ber 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.
|Σ ∩ sig(·)| SNOMED CT |Σ ∩ sig(·)| NCI
2 000 93.0% 5 000 97.0%
3 000 84.5% 10 000 81.1%
4 000 67.0% 15 000 72.0%
5 000 59.5% 20 000 59.2%
Table 1. Success rate of NUI
Fig. 4. Size distribution of MEX-modules and instance Σ-interpolants of SNOMED CT
First observe that neither SNOMED CT nor NCI contain any Σ-loops, for any sig-
nature Σ. 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 scenar-
ios. 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 com-
puted by NUI with the size of extracted Σ ∩ sig(·)-modules; i.e., minimal subsets of the
respective terminologies which preserve, e.g., inclusions between Σ ∩ sig(·)-concepts.
We use MEX-modules [5] of SNOMED CT and, respectively, >-local modules [2] 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 generated 100 random signatures with 3 000 concept names
and 20 role names in Σ ∩ sig(·). For 17 of those signatures, NUI failed to compute an
instance Σ-interpolant. For the remaining 83 signatures, Figure 4 shows the number of
interpolants and Σ ∩ sig(·)-modules (vertical axis) of a given size (horizontal axis). The
size of the Σ ∩sig(·)-modules lies between 125K and 150K symbols, which is about 3%
of SNOMED CT. 48.19% of instance Σ-interpolants are smaller than the corresponding
modules. However, 10 instance Σ-interpolants contain more than one million symbols
and the largest instance Σ-interpolant is more than 11 times larger than SNOMED CT.
For NCI, we computed instance Σ-interpolants and Σ ∩sig(·)-modules wrt. random
signatures with 7 000 concept names and 20 role names in Σ ∩ sig(·). NUI succeeded
Fig. 5. Size distribution of CEL-modules and instance Σ-interpolants of NCI
to compute interpolants for 97 of 100 signatures, each within 25 min. Figure 5 shows
the size distribution of the successfully computed interpolants and the corresponding
modules. The size of the Σ ∩ sig(·)-modules lies between 140K and 160K symbols,
which is about 22.5% of NCI. 74.47% of the instance Σ-interpolants are smaller than
the corresponding modules. On the other hand, 18 instance Σ-interpolants consist of
more than 400K symbols and 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,t , 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. [9, 19] consider forgetting in DL-Lite and [3] investigate in how far for-
getting in DLs can be reduced to forgetting in logic programs. [6], 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 exper-
imental 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 query languages. Many open problems remain; e.g., we con-
juncture 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 de-
cidability (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.
References
1. F. Baader, S. Brandt, and C. Lutz. Pushing the EL-envelope further. In Proceedings of
OWLED DC, 2008.
2. B. Cuenca Grau, I. Horrocks, Y. Kazakov, and U. Sattler. Just the right amount: Extracting
modules from ontologies. In Proceedings of WWW’07, pages 717–727, 2007.
3. T. Eiter, G. Ianni, R. Schindlauer, H. Tompits, and K. Wang. Forgetting in managing rules
and ontologies. In Web Intelligence, pages 411–419, 2006.
4. T. Eiter and K. Wang. Semantic forgetting in answer set programming. Artificial Intelligence,
172(14):1644–1672, 2008.
5. B. Konev, C. Lutz, D. Walther, and F. Wolter. Semantic modularity and module extraction in
description logic. In Proceedings of ECAI’08, pages 55–59, 2008.
6. B. Konev, D. Walther, and F. Wolter. The logical difference problem for description logic
terminologies. In Proceedings of IJCAR’08, pages 259–274, 2008.
7. B. Konev, D. Walther, and F. Wolter. Forgetting and uniform interpolation in large-scale
description logic terminologies. In Proceedings of IJCAI’09, 2009. To appear.
8. B. Konev, D. Walther, and F. Wolter. Forgetting and uniform interpolation in large-scale
description logic terminologies. Technical Report ULCS-09-006, University of Liverpool,
2009.
9. R. Kontchakov, F. Wolter, and M. Zakharyaschev. Can you tell the difference between DL-
lite ontologies. In Proceedings of KR’08, pages 285–295, 2008.
10. J. Lang, P. Liberatore, and P. Marquis. Propositional independence: formula-variable inde-
pendence and forgetting. Journal of Artificial Intelligence Research, 18:391–443, 2003.
11. C. Lutz, D. Walther, and F. Wolter. Conservative extensions in expressive description logics.
In Proceedings of IJCAI’07, pages 453–458, 2007.
12. C. Lutz and F. Wolter. Conservative extensions in the lightweight description logic EL. In
Proceedings of CADE’07, pages 84–99, 2007.
13. C. Lutz and F. Wolter. Deciding inseparability and conservative extensions in the description
logic EL. Journal of Symbolic Computation, 2009. To appear.
14. R. Reiter and F. Lin. Forget it! In Proceedings of AAAI Fall Symposium on Relevance, pages
154–159, 1994.
15. R. Rosati. On conjunctive query answering in EL. In Proceedings of DL’07, 2007.
16. N. Sioutos, S. de Coronado, M. Haber, F. Hartel, W. Shaiu, and L. Wright. NCI thesaurus:
a semantic model integrating cancer-related clinical and molecular information. Journal of
Biomedical Informatics, 40(1):30–43, 2006.
17. K. Spackman. Managing clinical terminology hierarchies using algorithmic calculation of
subsumption: Experience with SNOMED-RT. 2000.
18. A. Visser. Uniform interpolation and layered bisimulation. In Gödel ’96 (Brno, 1996),
volume 6 of Lecture Notes Logic. Springer Verlag, 1996.
19. Z. Wang, K. Wang, R. Topor, and J. Z. Pan. Forgetting in DL-Lite. In Proceedings of
ESWC’08, 2008.