=Paper=
{{Paper
|id=Vol-1193/paper_50
|storemode=property
|title=Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_50.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/KoopmannS14
}}
==Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes==
https://ceur-ws.org/Vol-1193/paper_50.pdf
Forgetting and Uniform Interpolation for
ALC-Ontologies with ABoxes
Patrick Koopmann,? Renate A. Schmidt
The University of Manchester, UK
{koopmanp, schmidt}@cs.man.ac.uk
Abstract. We present a method to compute uniform interpolants of
ALC-ontologies with ABoxes. Uniform interpolants are restricted views
of ontologies that only use a specified set of symbols, but share all entail-
ments in that signature with the original ontology. This way, it allows
to select or remove information from an ontology based on a signature,
which has applications in privacy, ontology analysis and ontology reuse.
We show that in general, uniform interpolants of ALC-ontologies with
ABoxes may require disjunctive statements or nominals in the ABox. An
evaluation of the method suggests however, that in most practical cases
uniform interpolants can be represented as a classical ALC-ontology.
1 Introduction
We present a method to compute uniform interpolants of ALC-ontologies with
ABoxes. Modern applications, especially in bio-informatics or medical domains,
often demand ontologies that cover a large vocabulary. With rising complexity,
these ontologies become harder to maintain and modify. Uniform interpolation
and forgetting deal with the problem of reducing the vocabulary used in an
ontology in such a way that all entailments over the reduced vocabulary are
preserved. In contrast to modules, uniform interpolants are completely in the
desired signature and may contain different axioms than the input ontology.
There are a range of applications for uniform interpolation. One can use it
to extract a part of an ontology for reuse, if only a subset of the terms defined
in the ontology is interesting for an application [21]. It also provides a way to
remove confidential information from an ontology to be shared among users with
different privileges [7]. By forgetting concepts that give structure to an ontology,
one can obfuscate it for other users [14]. Furthermore, uniform interpolants for
small signatures help exhibiting hidden relations in the ontology [8]. Further
applications are mentioned in [8, 16].
Uniform interpolation of TBoxes has been extensively studied in the descrip-
tion logic literature [22, 17, 16, 14, 11, 10, 9, 12], whereas forgetting symbols from
ABoxes has only gained little attention in the past. We think however that the
applications mentioned, especially in information hiding, clearly motivate the
study of uniform interpolation for ontologies with ABoxes.
?
Patrick Koopmann is supported by an EPSRC doctoral training award.
ALC-uniform interpolants preserve all entailments of the form C v D, C(a)
and r(a, b), where C, D and r are ALC-concepts and roles that only use con-
cept and role symbols from a specified signature. As it turns out, traditional
ALC-ontologies are not always sufficient to represent uniform interpolants that
preserve all these entailments. It is already known that cyclic definitions in the
TBox may require the use of fixpoint operators or additional symbols in the uni-
form interpolant [16, 11]. ABoxes bring a problem of a different nature, which
can be remedied by allowing disjunctions in the ABox of the uniform inter-
polant. ABoxes with disjunctions can be represented as classical ABoxes using
additional role symbols [2]. In order to represent the uniform interpolant fully
in the desired signature, we present an alternative approach using nominals.
To illustrate this, take as an example the ontology O containing the TBox
axiom A v ∀r.(¬B t A) and the ABox assertions r(a, b), r(b, a) and B(b).
The ALC-uniform interpolant of this ontology for Σ = {A, r} has to preserve
all ALC-entailments that only use A and r. This is the case for the ABox
A = {r(a, b), r(b, a), ¬A(a) ∨ A(b)}. A is therefore an ALC-uniform interpolant
of O for Σ. We can replace the disjunction in this ABox by the ALCO-concept
assertion (¬A t ∃r.({b} u A))(a). But in this case, it is impossible to preserve
all entailments of O in an ALC-ontology without disjunctions in the ABox. Our
evaluation suggests however, that in most practical cases uniform interpolants
can be represented without nominals or disjunctions.
In the next section we present the description logics used in this paper, and
give a formal definition of uniform interpolation. In Section 3, we describe a
method based on a new resolution calculus that is used to compute a clausal
representation of the uniform interpolant. The method introduces new symbols
to the signature, as well as disjunctions of concept assertions. In Section 4 we
describe how these introduced symbols are eliminated and how a uniform inter-
polant without disjunctions can be computed. The result may contain fixpoints
and nominals. Since fixpoints are not commonly supported by current descrip-
tion logic reasoners, we describe how uniform interpolants can be represented
in ALC, respectively ALCO, by either using additional symbols or approximat-
ing the uniform interpolant. We evaluate our method in Section 5 and give an
overview of related work in Section 6. We conclude with a short conclusion
in Section 7. Proofs of all lemmas and theorems can be found in the long version
of this paper [13].
2 Preliminaries
We present the description logics ALC, ALCµ, ALCO and ALCOµ, and give a
formal definition of disjunctive ABoxes and uniform interpolants.
Let Nc , Nr , Ni and Nv be four disjoint sets of respectively concept symbols,
role symbols, individuals and concept variables. ALCOµ-concepts are of the form
>, A, ¬C, C t D, ∃r.C, {a} and µX.C[X], where A ∈ Nc , r ∈ Nr , a ∈ Ni ,
X ∈ Nv , C and D are ALCOµ-concepts and C[X] is an ALCOµ-concept in
which X occurs positively (under an even number of negations) as a replacement
for a concept symbol. We define further concepts as abbrevations: ⊥ = ¬>, C u
D = ¬(¬C t ¬D), ∀r.C = ¬∃r.¬C, νX.C[X] = ¬µX.¬C[¬X] and {a1 , ..., an } =
{a1 } t . . . t {an }. µX.C[X] denotes the least fixpoint of C[X] and νX.C[X] the
greatest fixpoint.
A TBox T is a set of axioms, which are either concept inclusions C v D or
concept equivalence axioms C ≡ D, where C and D are ALCOµ-concepts. An
ABox A is a set of concept assertions C(a) and role assertions r(a, b), where
r ∈ Nr , a, b ∈ Ni and C is any ALCOµ-concept. An ontology O is a tuple
hT , Ai, where T is a TBox and A is an ABox. If an ontology does not contain
fixpoint expressions µX.C[X] or νX.C[X], it is an ALCO-ontology. If it does
not contain nominal expressions {a} or {a1 , ..., an }, it is an ALCµ-ontology. If it
contains neither nominals nor fixpoint expressions, it is in an ALC-ontology. In
the same way, we define ALC (ALCO, ALCµ) -axioms, -concepts and -assertions.
The semantics is defined as usual (see, e.g., [3] for ALCO and [4] for least
and greatest fixpoints). In particular, we write O |= α, where α is a concept
inclusion, concept assertion or role assertion, if α is true in all models of O.
A disjunctive concept assertion is of the form C1 (a1 ) ∨ . . . ∨ Cn (an ), where
the Ci are ALCOµ-concepts and the ai individuals, 1 ≤ i ≤ n. Given an ontology
O, let O|=C1 (a1 ) ∨ . . . ∨ Cn (an ) iff O |= Ci (ai ) for at least one 1 ≤ i ≤ n. A
disjunctive ABox is a set of role assertions, concept assertions and disjunctive
concept assertions. To make the distinction clear, we refer to ABoxes which do
not contain disjunctive concept assertions as classical ABoxes.
A signature Σ ⊆ (Nc ∪ Nr ) is a set of concept and role symbols. Given
a concept, axiom, assertion, TBox, ABox or ontology E, the signature of E,
denoted by sig(E), is the set of concept and role symbols occurring in E. Given
an ontology O and a signature Σ, OΣ is an ALC-uniform interpolant of O for Σ,
iff (i) sig(OΣ ) ⊆ Σ and (ii) OΣ |= α iff O |= α for every ALC-axiom and non-
disjunctive ALC-assertion α with sig(α) ⊆ Σ. Since we do not define any other
kinds of uniform interpolants, we refer to ALC-uniform interpolants simply as
uniform interpolants in the remainder of this paper. Note that we do not require
ALC-uniform interpolants to be expressed in ALC itself. We just require them
to preserve all entailments that can be expressed in ALC.
If Σ = sig(O) \ {x}, where x is a single concept or role symbol, we call the
uniform interpolant OΣ the result of forgetting x from O, and denote it by O−x .
3 Uniform Interpolation on ABoxes
The method for computing uniform interpolants works on a clausal form of the
input ontology, which uses an additional set of special concept symbols.
Definition 1. Let Nd ⊆ Nc be a set of designated concept symbols called de-
finers. A TBox literal is a concept of the form A, ¬A, ∃r.D or ∀r.D, where
A ∈ Nc and r ∈ Nr and D ∈ Nd . A TBox clause is a concept inclusion of the
form > v L1 t . . . t Ln , where each Li is a TBox literal. An ABox literal is
a concept assertion of the form L(a), where L is a TBox literal and a ∈ Ni .
An ABox clause is a disjunctive concept assertion of the form L1 ∨ . . . ∨ Ln ,
C1 t A C2 t ¬A
TBox Resolution:
C1 t C2
provided C1 ∪ C2 does not contain more than one negative definer-literal.
C1 t ∀r.D1 C2 t Qr.D2
TBox Role Propagation:
C1 t C2 t Qr.D12
where Q ∈ {∃, ∀} and D12 is a (possibly new) definer representing D1 u D2 ,
provided C1 ∪ C2 does not contain more than one negative definer-literal.
C t ∃R.D ¬D
TBox Existential Role Restriction Elimination:
C
Fig. 1. TBox rules
where every Li is an ABox literal. An ontology is in clausal form if its TBox
consists only of TBox clauses and its ABox consists only of ABox clauses and
role assertions.
We omit the leading ’> v’ in TBox clauses and assume that every clause is
represented as a set. This means, no literal appears twice in a clause and the
order of the literals is not important. Every ontology can be transformed into
clausal form using standard structural transformation techniques, where each
concept occurring under a role restriction ∃r.C or ∀r.C is replaced by a new
definer D, for which we add a new axiom D v C. The resulting ontology can
be brought into clausal form by applying standard conjunctive normal form
transformations. As a result, the TBox of the input ontology is represented by a
set of TBox clauses, and the ABox of the input ontology is represented by a set
of role assertions, ABox clauses as well as TBox clauses, which give meaning to
the introduced definer symbols. The transformation can be done in polynomial
time. Moreover, most ontologies are of a form that allows for a transformation
in nearly linear time.
Example 1 (Normal form). The ontology O = {A v ∀r.B, (C t ∀r.(A t ¬B))(a),
r(a, b)} is not in clausal form. The ontology N = {¬A t ∀r.D1 , ¬D1 t B, C(a) ∨
(∀r.D2 )(a), ¬D2 t A t ¬B, r(a, b)}, where D1 , D2 ∈ Nd , is in clausal form. N is
equi-satisfiable with O, and is therefore the clausal representation of O.
Literals of the form ¬D or ¬D(a), D ∈ Nd are called negative definer literals.
An important invariant of the described transformation, which our calculus pre-
serves, is that every TBox clause contains at most one negative definer literal
and that ABox clauses do not contain any negative definer literals. This invari-
ant ensures that we can always undo the structural transformation to eliminate
introduced definer symbols, to get back to the original signature of the ontology.
As shown in [11], the rules in Figure 1 can be used to both decide satisfiability
and compute uniform interpolants of ALC-TBoxes in clausal form. A difference
ABox Resolution:
C1 ∨ A(a) C2 ∨ ¬A(a) C1 t L C2 ∨ L(a)
C1 ∨ C2 C1 (a) ∨ C2
provided C1 ∪ C2 does not contain a negative definer literal.
ABox Role Propagation:
C1 ∨ (∀r.D1 )(a) C2 ∨ (Qr.D2 )(a) C1 ∨ (∀r.D1 )(a) C2 t Qr.D2
C1 ∨ C2 ∨ (Qr.D12 )(a) C1 ∨ C2 (a) ∨ (Qr.D12 )(a)
C1 t ∀r.D1 C2 ∨ (Qr.D2 )(a)
C1 (a) ∨ C2 ∨ (Qr.D12 )(a)
where Q ∈ {∃, ∀} and D12 is a (possibly new) definer representing D12 , provided
C1 ∪ C2 does not contain a negative definer literal.
Role Assertion Instantiation:
C1 ∨ (∀r.D)(a) r(a, b) C1 t ∀r.D r(a, b)
C1 ∨ D(b) C1 (a) ∨ D(b)
provided C1 ∪ C2 does not contain a negative definer literal.
ABox Existential Role Restriction Elimination:
C ∨ (∃r.D)(a) ¬D
C
Fig. 2. ABox Rules
to standard resolution calculi is that new definer symbols are introduced dynam-
ically during the process. If the role propagation rule is applied, and there is a
definer D12 for which N |= D12 v D1 u D2 holds, where N is our current set
of clauses, D12 is used in the conclusion. If such a definer does not exist, D12 is
introduced as a new definer and the clauses ¬D12 t D1 and ¬D12 t D2 are added
to the current clause set. This technique is key for termination of the calculus,
since only a finite number of definer symbols is introduced [11].
If the ontology is consistent, ABox assertions have no influence on entailed
concept inclusions. This means the TBox of the uniform interpolant can be com-
puted using the TBox rules. In order to compute the ABox of the uniform inter-
polant, we need the ABox rules shown in Figure 2. Define A = ¬A and ¬A = A,
and for any TBox clause C = L1 t . . . t Ln , let C(a) denote L1 (a) ∨ . . . ∨ Ln (a).
The ABox resolution, role propagation and existential role restriction elimina-
tion rules are adaptions of the corresponding TBox rules. The role assertion
instantiation rules make use of role assertions to propagate universal role re-
strictions. While the conclusion of every ABox rule is an ABox clause, the ABox
role propagation rules may introduce new definers, and thus lead to additional
TBox clauses in the current clause set.
Example 2 (ABox rules). Continuing on the clause set from the last example,
we can apply ABox role propagation on ¬A t ∀r.D1 and C(a) ∨ (∀r.D2 )(a),
which results in the clause ¬A(a) ∨ C(a) ∨ (∀r.D12 )(a), where D12 is a new
definer that is introduced with the two clauses ¬D12 t D1 and ¬D12 t D2 .
Applying role assertion instantiation on the new derived clause and r(a, b) results
in ¬A(a) ∨ C(a) ∨ D12 (b).
Since the number of introduced definers is bounded and clauses are represented
as sets, it can be verified that the saturation of any finite set of clauses by
the rules in Figure 1 and 2 is always finite. The calculus is also sound and
refutationally complete, as the following theorem shows.
Theorem 1. The TBox and ABox rules form a sound and refutationally com-
plete calculus and provide a decision procedure for satisfiability of ALC-ontologies
with non-empty TBoxes and ABoxes.
The calculus is used in the same way for forgetting concept and role symbols as
in [11, 9]. When forgetting a concept symbol A, the resolution rules only resolve
A and definers, and the role propagation and role assertion instantiation rules
are only applied if this makes new resolution steps on A possible.
When forgetting a role symbol r, the role assertion instantiation rule is ap-
plied for all role assertions with this r. Then the role propagation rules on r are
used to derive all clauses of the form C t ∃r.D and C ∨ (∃r.D)(a), where D is
an unsatisfiable definer. These existential restrictions are eliminated using the
existential role restriction elimination rules. In order to decide whether a definer
is unsatisfiable, we can either use our own calculus or an external reasoner. (For
a rule-based representation of this procedure, see [9].) Afterwards we remove all
clauses that containing the symbol A, respectively r, that we want to forget.
If our initial set of clauses is N, we denote the result by N−x , where x is
the symbol we want to forget. N−x is the clausal representation of the result of
forgetting x. In order to compute a uniform interpolant for a given signature Σ,
we iteratively forget every symbol x 6∈ Σ using this method.
Theorem 2. Let N be any set of TBox and ABox clauses and x any concept or
role symbol. Then, N−x |= α iff N |= α, for any ALC-axiom or ALC-assertion
α with x 6∈ sig(α).
4 Eliminating Definer Symbols and Disjunctive
Assertions
In this section we describe how the introduced definer symbols are eliminated,
and how the result can be represented in an ontology without disjunctive concept
assertions.
For eliminating definers, the same technique as in [11, 9] is used. First, all
TBox clauses that contain a positive definer literal of the form D and all ABox
Non-Cyclic Definer Elimination:
O ∪ {D v C}
provided D 6∈ sig(C)
O[D7→C]
Definer Purification:
O
provided D occurs only positively in O
O[D7→>]
Cyclic Definer Elimination:
O ∪ {D v C[D]}
provided D ∈ sig(C[D])
O[D7→νX.C[X]]
Fig. 3. Rules for eliminating definer symbols
clauses that contain literals of the form D(a) are removed. As shown in the
long version of this paper [13], these clauses are not needed to preserve en-
tailments in the desired signature, since all necessary inferences on them have
already been computed. In the resulting clause set, for every definer D, the set
of clauses of the form ¬D t Ci , 1 ≤ i ≤ n, is replaced by a single concept in-
clusion D v C1 u . . . u Cn . The resulting ontology is saturated using the rules
in Figure 3, where O[D7→C] denotes the result of replacing every definer D in O
by the concept C. These rules implement Ackermann’s Lemma [1] and its gen-
eralisation [18], which have been used in the context of second-order quantifier
elimination (see also [6]).
Theorem 3. Let O be an ALC-ontology and Σ ⊆ sig(O). Let OΣ be the result
of forgetting all symbols in sig(O) \ Σ from the clausal representation of O, and
eliminating all introduced definers. Then, OΣ is an ALC or ALCµ-ontology with
possibly disjunctive ABox, and OΣ is a uniform interpolant of O for Σ.
The cyclic definer elimination rule introduces fixpoint operators to the on-
tology. It is in general not always possible to find a finite uniform interpolant
without fixpoint operators. An alternative approach is to allow additional sym-
bols in the result, and simply not apply the cyclic definer elimination rule. By
keeping the cyclic definer symbols as “helper concepts” in the ontology, we ob-
tain an ontology that is not completely in the desired signature, but does not
use fixpoint operators and preserves all entailments we are interested in. A third
alternative is to approximate the fixpoint expressions in ALC as described in [11].
Using the role assertion instantiation rules, clauses with more than one indi-
vidual can be derived, which will be represented as disjunctive concept assertions
in the uniform interpolant. In general, there is no way to represent disjunctive
concept assertions as classical concept assertions in ALC if the respective indi-
viduals are connected by role assertions, as the following lemma shows.
Lemma 1. There are ALC-ontologies with disjunctive ABoxes that cannot be
approximated by a finite ALCµ-ontology with a classical ABox in such a way that
all entailments of the form C(a) or C v D are preserved, where C and D are
ALC-concepts. This even holds if the ontology contains no cyclic role assertions.
A consequence is that uniform interpolants of ALC-ontologies in general cannot
be represented by ALC or ALCµ-ontologies with classical ABoxes.
Theorem 4. There are ALC-ontologies O and signatures Σ, such that there
is no uniform interpolant of O for Σ that is a finite ALCµ-ontology without
disjunctive concept assertions.
A solution is to use nominals. If the individuals occurring in a disjunctive concept
assertions are connected via role assertions, the assertion can be transformed
using the following rule.
C ∨ C1 (a) ∨ C2 (b) r1 (a, a1 ) r2 (a1 , a2 ) . . . rn+1 (an , b)
(1)
C ∨ (C1 t ∃r1 . . . . ∃rn+1 .({b} u C2 ))(a)
If r(a, b) ∈ O, the concept ∃r.{b} is already satisfied by a. The concept asser-
tion (∃r.({b} u C2 )(a) states additionally that the individual b also satisfies C2 .
Therefore, concept assertions for b can be encoded inside concept assertions for
a, if there is some path along the role assertions from a to b.
If there is no chain of role assertions between two individuals a and b, we can-
not represent any information about b in a concept assertion of the form C(a).
This happens when the connecting role symbols have been removed from the
signature. However, it is possible to saturate clauses with unconnected indi-
viduals until these clauses are not needed anymore to preserve entailments
of the form C(a). For example, if the uniform interpolant contains A(a) and
¬A(a) ∨ B(b), we can also represent it by the classical ABox A = {A(a), B(b)}.
To make this approach practical, we use ordered resolution.
Let ≺ be any ordering between concept symbols and roles, and extend it to
a total ordering ≺l between TBox literals such that ∀r.D ≺ ∃r.D ≺ A ≺ ¬A for
all r ∈ Nr , D ∈ Nd and A ∈ Nc . Given an ABox clause C, a literal L(a) ∈ C is
maximal if for all literals of the form L0 (a) ∈ C we have L0 ≺l L. Observe that if
an ABox clause contains more than one individual name, it has more than one
maximal literal.
We further keep a set Md of marked definer symbols, which tells us which
additional clauses we have to saturate. At the beginning, this set is empty. A
clause is selected if it contains a pair of individuals that are not connected by a
chain of role assertions, or a literal of the form ¬D with D ∈ Md .
Given a set of clauses N, the set Nc is computed by saturating N using the
TBox and ABox rules of Figures 1 and 2, with the following side conditions.
– At least one clause in the premise of the rule must be selected.
– Each rule is only applied on the maximal literals of the clauses.
– If a maximal literal of selected clause is of the form ∃r.D or (∃r.D)(a), add D
to Md .
The set Nc is saturated using Rule (1), and all concept assertions containing
more than one individual are removed. We denote the result by NO . Since
Input Experiment Output
Ontology ABox Assertion ABox Assertion Disjunctive
Timeouts Duration
Assertions Size Assertions Size Assertions
Family 1,340 3.00 35.65% 69.3 sec. 2,093 7.63 73.37%
Semintec 65,189 2.72 6.57% 129.5 sec. 108,417 3.47 36.09%
UOBM 198,308 2.77 11.54% 200.1 sec. 217,265 3.58 80.62%
Fig. 4. Results for computing uniform interpolants with disjunctive ABox assertions.
Rule (1) produces concept assertions that are not clauses, but ALCO-assertions,
NO is not a clause set, but an ALCO-ontology.
Theorem 5. Let N be any set of clauses. Then, NO is an ALC or ALCO-
ontology with classical ABox, and we have NO |= α iff N |= α, where α is of the
form C v D, C(a) or r(a, b), and C and D are ALC-concepts.
Using this technique, uniform interpolants with disjunctions in the ABox can be
transformed to ALCO or ALCOµ-ontologies with classical ABox.
5 Evaluation
In order to investigate how our method performs in practice, we implemented it
in Scala1 using the OWL-API,2 with some of the optimisations described in [10].
Since we already evaluated uniform interpolation on TBoxes in [10] and [9], we
focused on ontologies which have an ABox that is large compared to the TBox.
The evaluation was based on three ontologies. Family3 is the family ontology
of Robert Stevens. It has a relatively complex TBox and its ABox consists only
of role assertions. Semintec4 is an ontology about bank transactions, and has a
simpler TBox but also a much larger ABox. The University Ontology Bench-
mark Generator (UOBM)5 comes with a tool that allows to generate ABoxes,
and has a more complex TBox than Semintec. For our evaluation we gener-
ated an ontology for one university. All ontologies have been reduced to ALC
by removing all axioms which are not in ALC, where we replaced domain and
range restrictions, as well as number restrictions of the form ≥1r.C and ≤0r.C
by equivalent expressions in ALC. We then generated 350 random signatures
for each ontology, where each symbol was assigned a probability of 25% to be
forgotten, and we computed uniform interpolants with and without disjunctive
assertions. The uniform interpolants were represented in ALC and ALCO re-
spectively using helper concepts, so that they could in theory be exported to
OWL. The timeout for each experimental run was set to 60 minutes.
1
http://www.scala-lang.org
2
http://owlapi.sourceforge.net
3
http://www.cs.man.ac.uk/~stevensr
4
http://www.cs.put.poznan.pl/alawrynowicz/semintec.htm
5
http://www.cs.ox.ac.uk/isg/tools/UOBMGenerator
Input Experiment Output
Ontology ABox Assertion ABox Assertion
Timeouts Duration Nominals
Assertions Size Assertions Size
Family 1,340 3.00 43.14% 376.0 sec. 1,400 5.35 6.03%
Semintec 65,189 2.72 6.57% 223.1 sec. 105,993 3.40 0.00%
UOBM 198,308 2.77 26.29% 442.9 sec. 191,965 3.18 0.00%
Fig. 5. Results for computing uniform interpolants with classical ABoxes.
The results for computing uniform interpolants with disjunctive ABoxes are
shown in Figure 4 and for computing uniform interpolants with classical ABoxes
in Figure 5. The table shows the number of assertions in the ABox, the average
size of an assertion of the respective ontology, the percentage of timeouts, the
average duration, the average sizes of the output and the percentage of uniform
interpolants that contained disjunctive assertions and nominals respectively.
Eliminating disjunctive assertions mostly took longer than forgetting the
symbols. But as a result, only in a few cases nominals were necessary in the uni-
form interpolant, so that the uniform interpolants could in most cases be repre-
sented as ALC-ontologies. Also, the uniform interpolants with classical ABox had
similar sizes to the respective input ontologies, except for the Semintec ontology.
If nominals were used, the respective assertions were usually very complex. The
timeouts were mainly caused by a small number of symbols. For example, for-
getting the concept Person from the Family ontology always lead to a timeout,
which caused 25% of the timeouts for this ontology.
We did not evaluate our method on ontologies with larger ABoxes, and there
are probably some optimisations possible for large ABoxes that will improve the
performance. However, in most realistic cases it is likely that, if the TBox is
fixed, the duration and the size of uniform interpolants are linear in the size of
the ABox, since individuals are usually not overly connected and the reasoner
can therefore process them in small independent groups for each symbol.
6 Discussion and Related Work
A lot of recent work covers uniform interpolation of TBoxes in description logics
of varying expressivity, including DL-Lite [22], EL [8, 17, 15], ALC [16, 20, 14, 11,
10], ALCH [9] and SHQ [12].
The first approach to compute uniform uniform interpolants of ALC-TBoxes
is based on a representation of the input ontology in disjunctive normal form,
from which incrementally a uniform interpolant is approximated [19], inspired by
earlier work on uniform interpolation of ALC-concepts [5]. This idea was further
developed in [21, 20] to make use of existing tableaux calculi.
Uniform interpolation of ALC-TBoxes is theoretically analysed in [16], where
it is shown that deciding whether a uniform interpolant can be represented
finitely without fixpoints is 2ExpTime-complete, and that the size of these uni-
form interpolants is in the worst case triple-exponentially with respect to the
size of the input ontology.
The early approaches for uniform interpolation in ALC required the input-
ontology to be either directly or effectively transformed into disjunctive normal
form, which is an unusual representation for ontologies. They also derive con-
sequences in an unrestricted way, which makes them unpractical for larger on-
tologies. Practical uniform interpolation requires a more goal-oriented approach,
which is followed in [14] and [11], where concept symbols are eliminated using
resolution. Whereas the method presented in [14] can only approximate uniform
interpolants in the general case, the algorithm in [11] always terminates with a
finite representation, which is achieved by using fixpoint operators. This method
was evaluated on a larger corpus in [10], showing that the worst case complexity
is hardly reached in practice and that for certain signatures uniform interpolants
can be computed in short amounts of time. In [9], the method was extended to
forgetting role symbols. The method also inspired a new calculus for uniform
interpolation in SHQ, which allows not only to interpolate more expressive on-
tologies, but also to preserve further entailments of ALC-ontologies [12].
Uniform interpolation involving ABoxes was first investigated for the light-
weight description logic DL-Lite [22]. Ontologies with ABoxes were also con-
sidered by the first approach for uniform interpolation in ALC [21]. But this
approach only works if the ABox is of a specific form, since the result is always
represented in ALC.
7 Conclusion and Future Work
We presented a method for uniform interpolation of ALC-ontologies with ABoxes.
In general, it is not always possible to represent these uniform interpolants
in ALC or using fixpoints. A solution is to either represent uniform interpolants
in ALCOµ or to allow disjunctions in the ABox. Our evaluation suggests how-
ever, that these cases do not occur often in practice, and that uniform inter-
polants of ALC-ontologies with large ABoxes can be practically computed in
most cases. We are currently working on extending the presented approach to
more expressive description logics, for example, with number restrictions or in-
verse roles.
In this work we focused on preserving entailments that are expressible in ALC.
Since the output of our method is represented in ALCOµ, it might be interesting
to preserve ALCO-entailments as well. There are some entailments of this sort
that our algorithm does not respect. For example, from the two ABox clauses
A(a) ∨ ¬B(a) and B(b) one can deduce (A t ¬{b})(a). Another restriction is
our uniform interpolants only preserve entailments of the form C v D, C(a)
and r(a, b). It would be interesting to investigate whether preserving further
entailments, such as conjunctive queries, is possible.
Our method can only be used for forgetting concept and role symbols. An
open question is how forgetting individuals can be performed. This would extend
the possibilities of the approach for applications such as information hiding.
References
1. Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathematis-
chen Logik. Mathematische Annalen 110(1), 390–413 (1935)
2. Areces, C., Blackburn, P., Hernandez, B.M., Marx, M.: Handling Boolean ABoxes.
In: Proc. DL’03. CEUR-WS.org (2003)
3. Baader, F., Nutt, W.: Basic description logics. In: Baader, F., Calvanese, D.,
McGuiness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.) The Description Logic
Handbook, chap. 2. Cambridge University Press, second edn. (2007)
4. Calvanese, D., Giacomo, G.D., Lenzerini, M.: Reasoning in expressive description
logics with fixpoints based on automata on infinite trees. In: Proc. IJCAI ’99. pp.
84–89. Morgan Kaufmann (1999)
5. ten Cate, B., Conradie, W., Marx, M., Venema, Y.: Definitorially complete de-
scription logics. In: Proc. KR’06. pp. 79–89 (2006)
6. Gabbay, D.M., Schmidt, R., Szalas, A.: Second Order Quantifier Elimination: Foun-
dations, Computational Aspects and Applications. College Publ. (2008)
7. Grau, B.C.: Privacy in ontology-based information systems: A pending matter.
Semantic Web 1(1-2), 137–141 (2010)
8. Konev, B., Walther, D., Wolter, F.: Forgetting and uniform interpolation in large-
scale description logic terminologies. In: Proc. IJCAI ’09. pp. 830–835. AAAI Press
(2009)
9. Koopmann, P., Schmidt, R.A.: Forgetting concept and role symbols in ALCH-
ontologies. In: Proc. LPAR’13. LNCS, vol. 8312, pp. 552–567. Springer (2013)
10. Koopmann, P., Schmidt, R.A.: Implementation and evaluation of forgetting in
ALC-ontologies. In: Proc. WoMO’13. CEUR-WS.org (2013)
11. Koopmann, P., Schmidt, R.A.: Uniform interpolation of ALC-ontologies using fix-
points. In: Proc. FroCoS’13. LNCS, vol. 8152, pp. 87–102. Springer (2013)
12. Koopmann, P., Schmidt, R.A.: Count and forget: Uniform interpolation of SHQ-
ontologies. In: Proc. IJCAR’14. Springer (2014), to appear.
13. Koopmann, P., Schmidt, R.A.: Forgetting and uniform interpolation of ALC-
ontologies with ABoxes—long version. Tech. rep., University of Manchester (2014),
http://www.cs.man.ac.uk/~koopmanp/DL_KoopmannSchmidt2014_long.pdf
14. Ludwig, M., Konev, B.: Towards practical uniform interpolation and forgetting for
ALC TBoxes. In: Proc. DL’13. pp. 377–389. CEUR-WS.org (2013)
15. Lutz, C., Seylan, I., Wolter, F.: An automata-theoretic approach to uniform in-
terpolation and approximation in the description logic EL. In: Proc. KR’12. pp.
286–296. AAAI Press (2012)
16. Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in ex-
pressive description logics. In: Proc. IJCAI ’11. pp. 989–995. AAAI Press (2011)
17. Nikitina, N.: Forgetting in general EL terminologies. In: Proc. DL’11. pp. 345–355.
CEUR-WS.org (2011)
18. Nonnengart, A., Szalas, A.: A fixpoint approach to second-order quantifier elimi-
nation with applications to correspondence theory. In: Logic at Work, pp. 307–328.
Springer (1999)
19. Wang, K., Wang, Z., Topor, R., Pan, J., Antoniou, G.: Concept and role forgetting
in ALC ontologies pp. 666–681 (2009)
20. Wang, K., Wang, Z., Topor, R., Pan, J.Z., Antoniou, G.: Eliminating concepts and
roles from ontologies in expressive descriptive logics. Computational Intelligence
(2012)
21. Wang, Z., Wang, K., Topor, R., Zhang, X.: Tableau-based forgetting in ALC on-
tologies. In: Proc. ECAI ’10. pp. 47–52. IOS Press (2010)
22. Wang, Z., Wang, K., Topor, R.W., Pan, J.Z.: Forgetting for knowledge bases in
DL-Lite. Ann. Math. Artif. Intell. 58(1–2), 117–151 (2010)