=Paper=
{{Paper
|id=Vol-1577/paper_14
|storemode=property
|title=Forgetting Concept and Role Symbols in ALCOIH\mu+(\top,\sqcap)-Ontologies
|pdfUrl=https://ceur-ws.org/Vol-1577/paper_14.pdf
|volume=Vol-1577
|authors=Yizheng Zhao,Renate A. Schmidt
|dblpUrl=https://dblp.org/rec/conf/dlog/ZhaoS16
}}
==Forgetting Concept and Role Symbols in ALCOIH\mu+(\top,\sqcap)-Ontologies==
https://ceur-ws.org/Vol-1577/paper_14.pdf
Forgetting Concept and Role Symbols in
ALCOIHµ+ (O, u)-Ontologies
Yizheng Zhao and Renate A. Schmidt
The University of Manchester, UK
Abstract. Forgetting is a non-standard reasoning problem that is con-
cerned with creating restricted views of ontologies relative to a subset
of the initial signature and preserving pertinent logical consequences up
to the symbols in the restricted views. In this paper, we present an
Ackermann-based approach for forgetting of concept and role symbols
in ontologies expressible in the description logic ALCOIHµ+ (O, u). The
method is one of only few approaches that can eliminate role symbols,
that can handle role inverse and ABox statements (via nominals), and
the only approach so far providing support for forgetting in description
logics with nominals. Despite the inherent difficulty of forgetting for this
level of expressivity, performance results with a prototypical implemen-
tation have shown very good success rates on real-world ontologies.
1 Introduction
This paper presents a practical forgetting method for creating restricted views of
ontologies expressed in the language of the description logic ALCOIHµ+ (O, u).
The work is motivated by the high demand for advanced techniques for ontology-
based knowledge processing. Research of forgetting, often referred to as uniform
interpolation (UI) in this area (or, variable elimination, projection or second-
order quantifier elimination in knowledge representation and logic) has gained
significant momentum since the work of various groups developing forgetting
methods for the description logic ALC and logics weaker than ALC, e.g., [11,
18, 19, 21, 25–27], and the foundational studies of the properties of forgetting
for description logics by, e.g., [10, 19, 20, 28]. These works give arguments for the
important role of forgetting in realising various tasks that are crucial for effective
processing and management of ontologies. For example, forgetting can be used
for ontology analysis and summary, for ontology reuse, for information hiding,
for computing the logical difference between ontologies, for ontology debugging
and repair, and for query answering.
Early work in the area primarily focused on forgetting concept symbols, as
role forgetting was realised to be significantly harder than forgetting of concept
symbols [28]. The dominant reason is probably that the result of forgetting role
symbols may not always be expressible in the source language. Although the
earliest work did study concept and role forgetting, e.g. [25], most subsequent
work considered only concept forgetting with the exception of [12–15]. Their
method can perform both concept and role forgetting for description logics ex-
tending ALC up to and including description logics with the expressiveness of
2 Yizheng Zhao and Renate A. Schmidt
SH, SIF and SHQ. In addition they have extended their method to forgetting
for description logics with ABoxes (for logics between ALC and SHI) [16].
The work on forgetting for description logics is predated by work on second-
order quantifier elimination [5–7], which can be traced to questions posed by
Boole and seminal work of [1]. These works triggered and influenced work in
knowledge representation [17], but also led to striking results in the automation
of correspondence theory of modal logics [3, 22]. Because of the close relationship
between description logics and modal logics, besides the work on modal corre-
spondence theory, investigations of UI for modal logics [4, 9, 24] are relevant.
These are particularly related to concept forgetting, but not to role forgetting.
The contribution of this paper is an approach for forgetting of concept and
role symbols in expressive description logics not considered so far. The method
accommodates ontologies expressible in the description logic ALCOIH and the
extension allowing positive occurrences of the least fixpoint operator µ, the top
role O and role intersection u. This means the method is one of only few ap-
proaches that can eliminate role symbols, while also handling role inverse and
ABox statements via nominals, and the only approach so far providing support
for forgetting in description logics with nominals. Being based on the Ackermann
approach to second-order quantifier elimination [5, 22, 29] the method terminates
always. We have shown the method is correct, i.e., the forgetting solution com-
puted is equivalent to the original ontology up to the symbols that have been
eliminated. A general problem of forgetting is marking out a language that is
expressive enough to allow for solutions to be expressed by finitely many formu-
las. Completeness results are rare and become harder to achieve with increased
expressivity, unless one is willing to admit second-order quantification, for which
the forgetting problem becomes trivially solvable. Despite our method not be-
ing complete, results of an evaluation with a prototypical implementation have
shown high success rates on real-world ontologies of various sizes.
2 The Description Logic ALCOIHµ+ (O, u)
Let NC , NR and NO be mutually disjoint sets of concept symbols (names), role
symbols (names) and individuals, respectively. Let Nµ be a set of concept vari-
ables disjoint with NC , NR and NO . Concepts in ALCOIH(O, u) have one of the
following forms: a | > | A | ¬C | C t D | ∀R.C, where a ∈ NO , A ∈ NC , C and D
are any ALCOIH(O, u)-concepts, and R is any role expression. Role expressions
in ALCOIH(O, u) can be the top role O, a role symbol r ∈ NR , the inverse r− of
a role symbol r, or a conjunction of these. The language of ALCOIHµ+ (O, u) ex-
tends that of ALCOIH(O, u) with atomic least fixpoint expressions of the form
µX.C[X], where X ∈ Nµ , and C[X] is a concept expression in which X occurs
only positively (under an even number of negations). Moreover, µ-expressions
may occur only positively. Because of this restriction, µ-expressions can be sim-
ulated in ALCOIH(O, u) with auxiliary concept symbols as in [13].
The semantics of the ALCOIH(O, u)-fragment is as expected. Intuitively,
µX.C[X] denotes the least general concept Cµ w.r.t. a concept expression for
Forgetting Concept and Role Symbols in ALCOIHµ+ (O, u)-Ontologies 3
which Cµ ≡ C[Cµ ] holds, where C[Cµ ] is a concept expression obtained from
replacing every occurrence of X in C[X] by Cµ . A formal definition of the se-
mantics of fixpoint expressions can be found in [2].
We assume without loss of generality that a TBox T is a set of concept axioms
of the form C v D, where C and D are closed concepts, i.e., contain no concept
variable not in the scope of a µ. An RBox R is a set of role axioms of the form
R v S, where R and S is a role symbol or an inverted role symbol. Nominals in a
description logic make ABox assertions superfluous, since these can be captured
by TBox inclusions via nominals. An ALCOIHµ+ (O, u)-ontology is therefore
assumed to be the union of the TBox and the RBox in this paper.
Theorem 1. Reasoning in ALCOIHµ+ (O, u) is decidable.
Theorem 1 follows from the decidability results of guarded fixpoint logic [8]
and the description logic ALBOid [23], which both subsume the languages of
ALCOIH(O, u) and ALCOIHµ+ (O, u).
In the sequel we describe the normal form on which our forgetting method
works. A TBox clause is a disjunction of ALCOIHµ+ (O, u)-concepts, in which
role expressions can be a role symbol, an inverted role symbol, or a conjunction
of these. A role literal is either a role symbol or an inverted role symbol, or their
negations. An RBox clause is a disjunction of two role literals of complementary
polarity. RBox clauses are transformed from the clausification of role axioms,
where role negation is introduced.
A clause that contains occurrences of a designated concept symbol and role
symbol S is called an S-clause. Given an S-clause C, an occurrence of S is posi-
tive in C if it is under an even number of negations. Otherwise it is negative. A
role symbol that occurs immediately under a (negated) universal role restriction
is assumed to be negative (positive). C is positive (negative) w.r.t. S if every oc-
currence of S in C is positive (negative). A set N of clauses is positive (negative)
w.r.t. S if every occurrence of S in N is positive (negative).
By sig(E) we denote the concept and role symbols occurring in E, where E
ranges over concepts, clauses, and ontologies. Σ is assumed to be the concept and
role symbols to be forgotten in this paper. Let S be any concept or role symbol
and let I and I 0 be interpretations. We say I and I 0 are equivalent up to S, or S-
equivalent, if I and I 0 coincide but differ possibly in the interpretations of S.
More generally, I and I 0 are equivalent up to Σ, or Σ-equivalent, if I and I 0 are
the same but differ possibly in the interpretations of the symbols in Σ.
Definition 1 (Forgetting in ALCOIHµ+ (O, u)-Ontologies). Let O and O0
be ALCOIHµ+ (O, u)-ontologies and let the signature be Σ ⊆ sig(O). O0 is
the solution of forgetting Σ-symbols in O, if the following conditions hold:
(i) sig(O0 ) ⊆ sig(O) and sig(O0 ) ∩ Σ = ∅, and (ii) for any interpretation I:
I |= O0 iff I 0 |= O, for some interpretation I 0 Σ-equivalent to I.
This states that the given ontology O and the forgetting solution O0 are
equivalent up to the interpretations of the symbols in Σ. It follows that if both O0
and O00 are solutions of forgetting symbols in Σ from O, then they are equivalent.
4 Yizheng Zhao and Renate A. Schmidt
3 Overview of the Forgetting Method
The forgetting process in our method consists mainly of three phases: the reduc-
tion to a set of ALCOIHµ+ (O, u)-clauses, the forgetting phase and the definer
elimination phase (see Figure 1).
Process to Transform to
Ontology O
set of clauses N r-reduced form
R
Ackermann
Σ
to forget r
Σ = {S1 , ..., S2 } into Analyser
Transform to
Σ
A-reduced form
C
Forgetting Elimination of Ackermann
0
Solution O Definer Symbols to forget A
Fig. 1. Overview of the forgetting method
Initially given, as the input to the method, are an ontology O of TBox and
RBox axioms expressible in ALCOIHµ+ (O, u), and a set Σ that contains the
concept and role symbols to be forgotten. The Σ-symbols are entirely determined
by the users and their application demands; Σ can thus be any subset of the
signature of the initial ontology as the user wishes. Once received by the system,
O is transformed into a set N of clauses, i.e., the normal form of our method.
The forgetting phase is an iteration of several rounds in which individual
concept and role symbols are eliminated. An important feature of the method
is that concept symbols and role symbols are forgotten in a focused way, that
is, the rules for concept forgetting and the rules for role forgetting are mutually
independent; concept and role symbols can thus be forgotten in any desired
order. In the forgetting phase, in order for the forgetting rules to be applied
to eliminate S ∈ Σ, the S-clauses must be transformed into S-reduced form.
Thus, whether the Σ-symbols are eliminable depends entirely on whether the
current set of clauses can be transformed into reduced form. This reduction is
performed using two Ackermann-based calculi working independently, which also
lead to goal-oriented elimination of the concept and role symbols. The calculi
are described in the next sections. Equivalence-preserving simplification rules
are applied throughout the forgetting process, ensuring that the current clauses
are always in simpler representations for efficiency. What the method returns, if
the forgetting is successful, is an ontology O0 that does not contain the symbols
in Σ, i.e., the returned ontology is formulated using only symbols in sig(O)\Σ.
Previous research has shown that the success rates of forgetting depend very
much on the order in which the Σ-symbols are forgotten [3, 5, 6, 14, 22], even
Forgetting Concept and Role Symbols in ALCOIHµ+ (O, u)-Ontologies 5
when forgetting only concept symbols, e.g., [29, 18]. An important challenge
therefore is to find good orders of eliminating Σ-symbols. Our method either
follows a user-specified order, or it uses a heuristic analysis based on the fre-
quency counts of the Σ-symbols, where concept symbols and role symbols are
analysed separately.
We refer to the maximal symbol of Σ w.r.t. the forgetting order as the
pivot in our method. Following (and starting with the pivot), the method
forgets the Σ-symbols one by one. If the pivot is successfully eliminated from N ,
we attempt to forget the next symbol in , which has become the new pivot.
Otherwise the pivot remains in Σ, flagged as a currently non-forgettable symbol,
and the next symbol in becomes the pivot. When the end of the ordering has
been reached, the calculus is applied to the flagged symbols, attempting again
to eliminate them. Success will always be pursued until a forgetting solution
is found. Though the ordering provides useful guidance during the forgetting
process, it does not generally guarantee the success of forgetting. On the symbols
not eliminated, a different ordering, not attempted before, will be used. When all
possible orderings have been attempted and there are still Σ-symbols remaining,
this means that the method fails to find a forgetting solution.
Theorem 2. For any ALCOIHµ+ (O, u)-ontology O and any Σ ⊆ sig(O), the
method always terminates and returns a set O0 of clauses. If O0 does not contain
any Σ-symbols, the method was successful. O0 is then a solution of forgetting the
symbols in Σ from O. If neither O nor O0 uses µ, O0 is Σ-equivalent to O in
ALCOIH(O, u). Otherwise, it is Σ-equivalent to O in ALCOIHµ+ (O, u).
4 Calculus for Concept Forgetting
We first present the calculus for forgetting of concept symbols in ontologies ex-
pressible in ALCOIHµ+ (O, u). The calculus extends the calculus of [29] for
concept forgetting in ALCOI. Since concept symbols occur only in TBox ax-
ioms, only the TBox needs to be processed for concept forgetting.
Non-Cyclic AckermannC Cyclic AckermannC
N , C1 t A, . . . , Cn t A N , C1 [A] t A, . . . , Cn [A] t A
A A
N¬C 1 t...t¬Cn
NµX.(¬C 1 t...t¬Cn )[X]
provided: (i) A does not occur in the provided: (i) the Ci are negative w.r.t.
Ci , and (ii) N is negative w.r.t. A. A, and (ii) N is negative w.r.t. A.
PurifyC,p PurifyC,n
N N
N is positive w.r.t. A. N is negative w.r.t. A.
N>A A
N¬>
Fig. 2. Forgetting concept symbol A in a set N of ALCOIHµ+ (O, u)-clauses
Definition 2 (A-Reduced Form). Suppose A is a concept symbol. A clause is
in A-reduced form if it is negative w.r.t. A, or it has the form A t C, where C is
an ALCOIHµ+ (O, u)-concept that (Case I) does not contain any occurrence
of A, or (Case II) is negative w.r.t. A. A set N of clauses is in A-reduced
form if every A-clause in N is in A-reduced form.
6 Yizheng Zhao and Renate A. Schmidt
The Ackermann and Purify rules, given in Figure 2, are the forgetting rules
that lead to the elimination of concept symbols in ALCOIHµ+ (O, u)-clauses.
Suppose A ∈ NC is the pivot and C is a concept expression, then NCA denotes
the set obtained from N by replacing every occurrence of A by C. We refer to
the clauses of the form Ci t A (1 ≤ i ≤ n) as positive premises of the rule. The
Ackermann rule is applicable (to forget A in N ) only if N is in A-reduced form.
Theorem 3 (Ackermann Lemma for Concept Forgetting). Let I be an
arbitrary ALCOIHµ+ (O, u)-interpretation. For A the pivot, when the Non-
Cyclic AckermannC rule is applicable, the conclusion of the rule is true in I
iff for some interpretation I 0 A-equivalent to I, the premises are true in I 0 . The
same is true for the Cyclic AckermannC rule and the PurifyC,p(n) rules.
This states that eliminating the pivot symbol in NC with the AckermannC
and PurifyC rules preserves equivalence up to the pivot. Given the pivot A and
a set N of clauses in A-reduced form, the Non-Cyclic Ackermann rule is applied
when A does not occur in the Ci (1 ≤ i ≤ n) of the positive premises. The
Cyclic Ackermann rule is applied when A occurs in the Ci but only negatively,
e.g., A occurs in a cyclic clause ¬∀r.A t A. Fixpoints are introduced in this case
in order to facilitate finite representation of the result, where every occurrence
of A in ¬C1 t . . . t ¬Cn is replaced by X, a fresh concept variable, and every
occurrence of A in N is replaced by µX.(¬C1 t . . . t ¬Cn )[X]. The Purify rule
is applied whenever A is pure in N , i.e., N is positive (or negative) w.r.t. A.
Concept Clausify Case Splitting
N , C t ¬(D1 t . . . t Dn ) N , ¬a t C1 t . . . t Cn
N , C t ¬D1 , . . . , C t ¬Dn N , ¬a t C1 | . . . | ¬a t Cn
provided: A has positive occurrences provided: A occurs positively in C1 t
in ¬(D1 t . . . t Dn ). . . . t Cn .
SkolemizationO SkolemizationR
N , C t ¬∀O.D N , ¬a t ¬∀R.C
N , ¬b t ¬D t ∀O.C N , ¬a t ¬∀R.¬b, ¬b t ¬C
provided: (i) b is a fresh nominal, and provided: (i) b is a fresh nominal, and
(ii) A occurs positively in ¬∀O.D. (ii) A occurs positively in ¬∀R.C.
Concept Surfacing Sign Switching
N , C t ∀R.D N
N , (∀R− .C) t D (N¬A A ¬¬A
)A
provided: (i) A does not occur pos- provided: (i) Sign Switching has not
itively in C, and (ii) A occurs posi- been performed on A, and (ii) N is
tively in ∀R.D. closed to other rewrite rules.
Fig. 3. The rewrite rules for finding A-reduced form of N
Clauses are usually not given in reduced form initially. Figure 3 lists the
set of rewrite rules for finding the A-reduced form of a set of clauses for A the
pivot. The Case Splitting rule splits the derivation into several branches. The
intermediate forgetting solution returned at the end of a symbol elimination
round is the disjunction of the solutions of each branch in the derivation. New
compared to [29], besides the Cyclic Ackermann rule, is the SkolemizationO rule
Forgetting Concept and Role Symbols in ALCOIHµ+ (O, u)-Ontologies 7
that rewrites the existential quantification in the premise by the introduction
of a fresh nominal. Crucial for the practicality of the method are a number of
equivalence-preserving simplification rules, not described here though.
5 Calculus for Role Forgetting
The main contribution of this paper is a calculus for forgetting of role symbols
in ontologies expressible in ALCOIHµ+ (O, u). Since role symbols occur in the
TBox and the RBox, both need to be processed when role symbols are forgotten.
Definition 3 (r-Reduced Form). Suppose r is a role symbol. A clause is in
r-reduced form if it has the form C t ∀r.D or C t ¬∀(r u Q).D, where C and
D are ALCOIHµ+ (O, u)-concepts that do not contain any occurrence of r and
Q is an ALCOIHµ+ (O, u) role expression that does not contain any occurrence
of r; or it has the form ¬S t r or S t ¬r, where S ∈ {s, s− } for s (6= r) a role
symbol. A set N of clauses is in r-reduced form if every r-clause in N is in
r-reduced form.
As in concept forgetting, the pivot-clauses are first transformed into pivot-
reduced form, so that the Ackermann rule for role forgetting becomes applicable.
Finding pivot-reduced form of a clause is not always possible unless definer sym-
bols are introduced. Definer symbols are specialised concept symbols that do not
occur in the present ontology [13], and are introduced as follows: given a clause
of the form C t ∀r(−) .D or C t ¬∀r(−) .D, with r being the pivot and occur-
ring in Q ∈ {C, D}, the definer symbols are used as substitutes, incrementally
replacing C and D until C and D do not contain any occurrences of r. A new
clause ¬D t Q is added to the clause set for each replaced sub-concept Q, where
D is a fresh definer symbol. For example, introducing a definer symbol D1 leads
to A t ∀r.¬∀r.B being rewritten with A t ∀r.D1 and ¬D1 t ¬∀r.B, where A
and B are concept symbols. The definer symbols are eliminated using the rules
for concept forgetting once all role symbols in Σ have been forgotten. It is for
this reason that our system defaults to forgetting role symbols first so that the
definer symbols can be eliminated as part of subsequent concept forgetting.
Role Surfacing to TBox Role Surfacing to RBox
N , C t ∀r− .D N , ¬S t r− N , S t ¬r−
−
N , ¬S t r N , S − t ¬r
N , D t ∀r.C
provided: r is a role symbol that does provided: S is either a role symbol or
not occur in C and D. an inverted role symbol.
Fig. 4. The rewrite rules for finding r-reduced form of N
Since the underlying language accommodates role inverse, the calculus in-
cludes two Role Surfacing rules, shown in Figure 4, in order to reformulate
expressions without occurrences of inverses of the pivot in the respective TBox
and RBox clauses, so that the other rules in the calculus do not need to cater
for role inverse. The Role Surfacing rules are applied after definer symbols have
been introduced, and before the application of the forgetting rules.
8 Yizheng Zhao and Renate A. Schmidt
AckermannR
+ +
PT PR
z }| { z }| {
N , C 1 t ¬∀r u Q1 .D1 , . . . , C k t ¬∀r u Qk .Dk , ¬T 1 t r, . . . , ¬T u t r ,
P−T P−
R
z }| { z }| {
C1 t ∀r.D1 , . . . , Cm t ∀r.Dm , ¬r t S1 , . . . , ¬r t Sn
N , T -BlockH (1, m), . . . , T -BlockH (k, m) ,
R-BlockC (1, m), . . . , R-BlockC (u, m) , R-BlockR (1, n), . . . , R-BlockR (u, n)
? T -BlockH (j, m) is the set (1 ≤ j ≤ k):
{C j t C Y t ¬∀Hj .(Dj t DY )|Y ⊆ [m]}, where
¬> if Y = ∅ ¬> if Y = ∅
CY = F
Ci otherwise, D Y
= F
¬Di otherwise, and
i∈Y i∈Y
− −
Hj = S1 u . . . u Sn u Qj if PR 6= ∅, otherwise (PR = ∅) Hj = O u Qj .
? R-BlockC (l, m) is the set {C1 t ∀T l .D1 , . . . , Cm t ∀T l .Dm } (1 ≤ l ≤ u).
? R-BlockR (l, n) is the set {¬T l t S1 , . . . , ¬T l t Sn } (1 ≤ l ≤ u).
provided: r is the pivot that does not occur in N , and N is in r-reduced form.
PurifyR
N
r
provided: N is positive (negative) w.r.t. r, where r is the pivot.
N(¬)O
Fig. 5. Forgetting role symbol r in a set N of ALCOIHµ+ (O, u)-clauses
Theorem 4 (Ackermann Lemma for Role Forgetting). Let I be an arbi-
trary ALCOIHµ+ (O, u)-interpretation. For r the pivot, when the AckermannR
or PurifyR rule in Figure 5 is applicable then the conclusion of the rule is true
in I iff for some interpretation I 0 r-equivalent to I, the premises are true in I 0 .
Given a set N of clauses with r ∈ NR being the pivot, once N has been
transformed into r-reduced form, we apply the AckermannR rule and the PurifyR
rule given in Figure 5 to eliminate r. By definition, clauses in r-reduced form
have four distinct forms. We refer to the clauses of the form C j t ¬∀r u Qj .Dj
(1 ≤ j ≤ k) as positive TBox premises (denoted by PT+ ) and clauses of the form
Ci t ∀r.Di (1 ≤ i ≤ m) as negative TBox premises (denoted by PT− ) of the rule.
We refer to the clauses of the form ¬T l t r (1 ≤ l ≤ n) as positive RBox premises
+
(denoted by PR ) and clauses of the form ¬r t Si (1 ≤ i ≤ u) as negative RBox
−
premises (denoted by PR ) of the rule. Since it is possible for r to occur in any
of these premises (and the premises do not necessarily wholly exist), there are
several situations where the AckermannR rule is applicable. For different PT−
−
and PR the AckermannR rule is performed as follows.
Case (I): If PT− 6= ∅ and PR −
6= ∅, then PT− and PR −
(the negative premises)
+ + +
are combined with every clause in PT (if PT 6= ∅) and every clause in PR
+
(if PR 6= ∅), which leads to the elimination of r, and a forgetting solution O0
where r 6∈ sig(O0 ). Specifically, combining PT− and PR −
with one of the positive
Forgetting Concept and Role Symbols in ALCOIHµ+ (O, u)-Ontologies 9
TBox premises (PT+ ) leads to a set of TBox clauses (denoted by T -Block H (j, m)),
−
where Hj is the conjunction of Qj and the Si (1 ≤ i ≤ n) occurring in PR (Hj :=
Q u S1 u . . . u Sn ), m denotes the number of negative TBox premises (|PT− |),
j
and j refers to the positive TBox premise with which PT− and PR −
combine. [m]
j Y j j Y
denotes the set {1, . . . , m}, and {C t C t ¬∀H .(D t D )|Y ⊆ [m]} is the
set that contains all clauses corresponding to every assignment of Y .
The following example illustrates this case. Given Σ = {r} and a set N of
clauses in r-reduced form with PT− = {A1 t ∀r.B1 , A2 t ∀r.B2 }, PR −
= {¬r t
− + − −
s1 , ¬r t s2 }, and A t ¬∀r.B ∈ PT , combining PT and PR with A t ¬∀r.B leads
to T -Block H (j, m) = {A t C Y t ¬∀(s1 u s− Y
2 ).(B t D )|Y ⊆ [2]} that consists of
the following clauses:
¬> t¬∀(s1 u s−
1. A t |{z} 2 ).(B t |{z}
¬> ) when Y = ∅
CY DY
2. A t A1 t¬∀(s1 u s−
2 ).(B t ¬B ) when Y = {1}
|{z} |{z}1
CY DY
3. A t A2 t¬∀(s1 u s−
2 ).(B t ¬B ) when Y = {2}
|{z} |{z}2
CY DY
4. A t A1 t A2 t¬∀(s1 u s−
2 ).(B t ¬B t ¬B2 ) when Y = {1, 2}
| {z } | 1 {z }
CY DY
Combining PT− with one of the positive RBox premises leads to a set of
TBox clauses (denoted by R-Block C (l, m)), where m are the negative TBox
premises and l refers to the positive RBox premise with which PT− combines;
−
combining PR with one of the positive RBox premises leads to a set of RBox
clauses (denoted by R-Block R (l, n)), where n are the negative RBox premises
−
and l refers to the positive RBox premise with which PR combines.
Case (II): If PT 6= ∅ and PR = ∅, then combining PT− with one of the
− −
positive TBox premises leads to the same result as in Case (I) (T -Block H (j, m)),
only that a top role (O) replaces S1 u . . . u Sn , i.e., H = O. Combining PT− with
one of the positive RBox premises leads to the same result as in Case (I), i.e.,
R-Block C (l, m) (1 ≤ l ≤ u). Case (III): If PT− = ∅ and PR −
6= ∅, then combining
−
PR with one of the positive TBox premises and with one of the positive RBox
premises leads to the same results as in Case (I), i.e., T -Block H (j, m) (1 ≤ j ≤ k)
and R-Block R (l, n) (1 ≤ l ≤ u) respectively. Case (IV): The case PT− = ∅ and
−
PR = ∅ can be seen as an instance of the case where r is pure. The pivot is
eliminated using the PurifyR rule in this case.
The pivot is forgotten in the ontology once every positive premise (in PT+
and PR +
) has been combined with PT− (if PT− 6= ∅) and PR − −
(if PR 6= ∅). Given a
set of clauses in pivot-reduced form with m negative TBox premises (|PT− | = m),
−
n negative RBox premises (|PR | = n), k positive TBox premises (|PT+ | = k), and
u positive RBox premises (|PR | = u), combining PT− and PR
+ −
with all positive
TBox premises yields a set of k · 2m clauses (exponential growth); combining
PT− and PR −
with all positive RBox premises yields a set of um + un clauses
(polynomial growth). The size of the forgetting solution therefore depends largely
on the number of the negative TBox premises (m).
10 Yizheng Zhao and Renate A. Schmidt
6 Evaluation and Empirical Results
We implemented a prototype of the forgetting method in Java using the OWL-
API1 , and conducted a number of experiments on real-world ontologies that are
taken from the NCBO BioPortal2 and Oxford Ontology3 repositories to evaluate
the practicality of the method. The experiments were run on a desktop with an
Intelr Coretm i7-4790 processor, and four cores running at up to 3.60 GHz and
8 GB of DDR3-1600 MHz RAM. The ontologies used for our evaluation were
restricted to ALCOIH(O, u)-fragments, and any sub-concepts beyond the scope
of ALCOIH(O, u) were replaced by >. Consequently, 180 and 200 ontologies
of various sizes were selected from the NCBO BioPortal and Oxford Ontology
Library, respectively. We repeated the experiments 100 times on each ontology
and averaged the results to verify the accuracy of our findings.
To fit in with real-world applications such as computing logical difference
between ontologies and predicate hiding, where forgetting a small number of
symbols is in demand, we set up a series of experiments where we forgot 10% and
30% of concept and role symbols that were randomly selected in each ontology.
There are also situations where it would be of interest to forget a large number
of symbols; ontology reuse is such an example [12–15]. We therefore set up a
series of experiments with a large number of concept and role symbols to be
forgotten (80% of the concept symbols and 50% of the role symbols in the initial
signature). The heuristic for determining the order of eliminating concept and
roles symbols ( C and R ) was also tested. The Σ-symbols were eliminated in
the order as returned by the OWL-API function that gets all concept symbols in
the ontology, when the heuristic was not applied. We started with the evaluation
of concept symbol forgetting, where a timeout of 15 minutes was imposed.
Input Setting Results Setting Results
Ontology |Σ| (%) C Time (sec.) Timeout Success R. Fixp. |Σ| (%) R Definer in Time (sec.) Success R. Clause ↑
7 4.890 0.0% 100.0% 0.0% 7 1.1/onto. 2.120 sec. 100.0% 4.1%
20 (10%) 4 (10%)
3 3.260 0.0% 100.0% 0.0% 3 10 onto. 2.101 sec. 100.0% 4.1%
7 18.672 4.4% 94.4% 7.2% 7 1.9/onto. 8.658 sec. 100.0% 14.5%
BioPortal 60 (30%) 12 (30%)
3 9.336 1.1% 98.3% 7.8% 3 13 onto. 8.314 sec. 100.0% 14.5%
(354 Axioms
7 70.416 13.8% 83.3% 13.3% 7 3.0/onto. 20.913 sec. 100.0% 26.5%
on Avg.) 160 (80%) 20 (50%)
3 29.340 5.6% 91.7% 17.2% 3 16 onto. 20.566 sec. 100.0% 26.5%
7 31.326 6.3% 92.6% 6.8% 7 2.0/onto. 10.564 sec. 100.0% 15.0%
80 Avg. Avg.
3 13.979 2.4% 96.7% 8.3% 3 13 onto. 10.327 sec. 100.0% 15.0%
7 44.392 3.0% 97.0% 0.5% 7 2.4/onto. 3.187 sec. 100.0% 2.2%
36 (10%) 5 (10%)
3 27.745 1.5% 98.5% 0.5% 3 25 onto. 3.072 sec. 100.0% 2.2%
7 193.106 17.0% 79.5% 11.5% 7 3.7/onto. 18.537 sec. 100.0% 6.9%
Oxford 108 (30%) 15 (30%)
3 80.461 9.5% 88.5% 14.5% 3 28 onto. 17.998 sec. 100.0% 6.9%
(875 Axioms
7 412.852 34.5% 61.5% 19.0% 7 5.7/onto. 36.292 sec. 100.0% 14.6%
on Avg.) 288 (80%) 25 (50%)
3 166.270 17.5% 78.5% 26.5% 3 39 onto. 34.117 sec. 100.0% 14.6%
7 216.783 18.2% 79.3% 10.3% 7 3.9/onto. 19.339 sec. 100.0% 7.9%
144 Avg. Avg.
3 91.492 9.5% 88.5% 13.8% 3 30 onto. 18.396 sec. 100.0% 7.9%
Fig. 6. Results for concept forgetting Fig. 7. Results for role forgetting
The results (of forgetting only concept symbols) obtained from forgetting
10%, 30% and 80% of the concept symbols from the respective BioPortal and
Oxford ontologies are shown in Figure 6, which is quite revealing in several
ways. The most notable observation to emerge from the results is that, with the
1
http://owlapi.sourceforge.net/
2
http://bioportal.bioontology.org/
3
http://www.cs.ox.ac.uk/isg/ontologies/
Forgetting Concept and Role Symbols in ALCOIHµ+ (O, u)-Ontologies 11
heuristically determined elimination order (indicated by 3), our implementation
was successful (forgot all Σ-symbols) in 96.7% of the BioPortal-cases within a
limited period of time, with 8.3% of them using fixpoints in the result. In the
case of 10% of the concept symbols specified to be forgotten, the success rate
rose to 100%. Even without the heuristic (7), the forgetting solution could be
found by our implementation in 92.6% of the cases. Since the Oxford ontologies
were more than twice as large as the BioPortal ontologies and a larger set of
concept symbols was specified to be forgotten, a reduction in the performance
was expected. The implementation was unable to compute the solution in 11.5%
of the Oxford-cases, and in 13.8% of the solved cases fixpoints occurred in the
result. The use of the heuristic boosted the overall success rate by 4% and 9.2%,
and improved the time efficiency by 124.1% and 136.9% in the BioPortal and
Oxford ontologies, respectively.
We also evaluated the performance of forgetting different number of role
symbols with the same ontologies used for the evaluation of concept forgetting
(using a timeout of 5 minutes). The results (of forgetting only role symbols)
are shown in Figure 7, from which it can be seen that our method successfully
eliminated the role symbols in Σ in all cases. The time used for forgetting role
symbols, as expected, was significantly longer than forgetting the same number
of concept symbols, despite the 100% success rate. Because of the nature of the
AckermannR rule, role symbol forgetting leads to growth of clauses in the forget-
ting solution, which was however modest (Clause ↑) compared to the theoretical
worst case. Definer symbols were introduced only in a small proportion of the
ontologies to help conversion to reduced form. This indicates that most clauses
in the ontologies were flat. By m/onto, we mean that there were m definer sym-
bols introduced in each ontology, and by n onto we mean that n ontologies out
of the total introduced the definer symbol.
7 Conclusion and Future Work
In this paper we have developed a method of concept and role forgetting for
expressive description logics with nominals, non-empty TBoxes and ABoxes, and
a rich language for expressing properties of roles. The method can handle role
inclusion statements, role conjunctions and role inverses. This is extremely useful
from the perspective of ontology engineering as it increases the arsenal of tools
available to create restricted views of ontologies. The results of the evaluation
on real-world ontologies has shown that often fixpoints and role conjunction are
not needed to express forgetting solutions, and overall the performance results
are very positive.
Currently beyond the scope of our method are forgetting transitive roles. We
can extend the method to eliminate concept symbols in the presence of transitive
roles, but the interaction between transitive roles and role hierarchy inclusion
statements can lead to results where it is not clear how to represent them finitely.
The problem of extending the method to handle number restrictions remains
completely open; possibly the techniques of [14, 15] can help extend the method.
12 Yizheng Zhao and Renate A. Schmidt
References
1. W. Ackermann. Untersuchungen über das Eliminationsproblem der mathematis-
chen Logik. Mathematische Annalen, 110(1):390–413, 1935.
2. D. Calvanese, G. De Giacomo, and M. Lenzerini. Reasoning in expressive descrip-
tion logics with fixpoints based on automata on infinite trees. In Proc. IJCAI’99,
pages 84–89. Morgan Kaufmann, 1999.
3. W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and
completeness in modal logic. I. The core algorithm SQEMA. Logical Methods in
Computer Science, 2(1), 2006.
4. G. D’Agostino and M. Hollenberg. Logical questions concerning the µ-Calculus:
Interpolation, Lyndon and Los-Tarski. J. Symb. Log., 65(1):310–332, 2000.
5. P. Doherty, W. Lukaszewicz, and A. Szalas. Computing circumscription revisited:
A reduction algorithm. Journal of Automated Reasoning, 18(3):297–336, 1997.
6. D. M. Gabbay and H. J. Ohlbach. Quantifier elimination in second–order predicate
logic. In Proc. KR’92, pages 425–435. Morgan Kaufmann, 1992.
7. D. M. Gabbay, R. A. Schmidt, and A. Szalas. Second Order Quantifier Elimination:
Foundations, Computational Aspects and Applications. College Publications, 2008.
8. E. Grädel and I. Walukiewicz. Guarded fixed point logic. In Proc. LICS’99, pages
45–54. IEEE Computer Society, 1999.
9. A. Herzig and J. Mengin. Uniform interpolation by resolution in modal logic. In
Proc. JELIA’08, volume 5293 of Lecture Notes in Computer Science, pages 219–
231. Springer, 2008.
10. B. Konev, C. Lutz, D. Walther, and F. Wolter. Model-theoretic inseparability and
modularity of description logic ontologies. Artificial Intelligence, 203:66–103, 2013.
11. B. Konev, D. Walther, and F. Wolter. Forgetting and uniform interpolation in
extensions of the description logic EL. In Proc. DL’09, volume 477 of CEUR
Workshop Proceedings. CEUR-WS.org, 2009.
12. P. Koopmann and R. A. Schmidt. Forgetting concept and role symbols in ALCH-
ontologies. In Proc. LPAR’13, volume 8312 of Lecture Notes in Computer Science,
pages 552–567. Springer, 2013.
13. P. Koopmann and R. A. Schmidt. Uniform interpolation of ALC-ontologies using
fixpoints. In Proc. FroCos’13, volume 8152 of Lecture Notes in Computer Science,
pages 87–102. Springer, 2013.
14. P. Koopmann and R. A. Schmidt. Count and forget: Uniform interpolation of
SHQ-ontologies. In Proc. IJCAR’14, volume 8562 of Lecture Notes in Computer
Science, pages 434–448. Springer, 2014.
15. P. Koopmann and R. A. Schmidt. Saturated-based forgetting in the description
logic SIF. In Proc. DL’15, volume 1350 of CEUR Workshop Proceedings. CEUR-
WS.org, 2015.
16. P. Koopmann and R. A. Schmidt. Uniform interpolation and forgetting for ALC-
ontologies with ABoxes. In Proc. AAAI’15, pages 175–181. AAAI Press, 2015.
17. F. Lin and R. Reiter. Forget it! In Proc. AAAI Fall Symposium on Relevance,
pages 154–159, 1994.
18. M. Ludwig and B. Konev. Practical uniform interpolation and forgetting for ALC
TBoxes with applications to logical difference. In Proc. KR’14. AAAI Press, 2014.
19. C. Lutz, I. Seylan, and F. Wolter. An automata-theoretic approach to uniform
interpolation and approximation in the description logic EL. In Proc. KR’12,
pages 286–297. AAAI Press, 2012.
Forgetting Concept and Role Symbols in ALCOIHµ+ (O, u)-Ontologies 13
20. C. Lutz and F. Wolter. Foundations for uniform interpolation and forgetting in
expressive description logics. In Proc. IJCAI’11, pages 989–995. IJCAI/AAAI,
2011.
21. N. Nikitina and S. Rudolph. (Non-)Succinctness of Uniform Interpolants of General
Terminologies in the Description Logic EL. Artificial Intelligence, 215:120–140,
2014.
22. R. A. Schmidt. The Ackermann approach for modal logic, correspondence theory
and second-order reduction. Journal of Applied Logic, 10(1):52–74, 2012.
23. R. A. Schmidt and D. Tishkovsky. Using tableau to decide description logics with
full role negation and identity. ACM Trans. Comput. Log., 15(1):7:1–7:31, 2014.
24. A. Visser. Bisimulations, Model Descriptions and Propositional Quantifiers. Logic
Group Preprint Series. Department of Philosophy, Utrecht Univ., 1996.
25. K. Wang, Z. Wang, R. Topor, J. Z. Pan, and G. Antoniou. Concept and role
forgetting in ALC ontologies. In Proc. ISWC’09, volume 5823 of Lecture Notes in
Computer Science, pages 666–681. Springer, 2009.
26. K. Wang, Z. Wang, R. Topor, J. Z. Pan, and G. Antoniou. Eliminating concepts and
roles from ontologies in expressive description logics. Computational Intelligence,
30(2):205–232, 2014.
27. Z. Wang, K. Wang, R. Topor, and J. Z. Pan. Forgetting for knowledge bases in
DL-Lite. Annals of Mathematics and Artificial Intelligence, 58(1-2):117–151, 2010.
28. Z. Wang, K. Wang, R. W. Topor, and J. Z. Pan. Forgetting concepts in DL-Lite.
In Proc. ESWC’08, volume 5021 of Lecture Notes in Computer Science, pages
245–257. Springer, 2008.
29. Y. Zhao and R. A. Schmidt. Concept Forgetting in ALCOI-Ontologies Using
an Ackermann Approach. In Proc. ISWC’15, volume 9366 of Lecture Notes in
Computer Science, pages 587–602. Springer, 2015.