Forgetting refers to a non-standard reasoning problem concerned with eliminating concept and role symbols from description logic-based ontologies while preserving all logical consequences up to the remaining symbols. Whereas previous research has primarily focused on forgetting concept symbols, in this paper, we turn our attention to role symbol forgetting. In particular, we present a practical method for semantic role forgetting for ontologies expressible in the description logic ALCOQH(O), i.e., the basic description logic ALC extended with nominals, number restrictions, role inclusions and the universal role. Being based on an Ackermann approach, the method is so far the only approach for forgetting role symbols in description logics with number restrictions. The method is goal-oriented and incremental. It always terminates and is sound in the sense that the forgetting solution is equivalent to the original ontology up to the forgotten symbols, possibly with new concept definer symbols. Despite our method not being complete, performance results of an evaluation with a prototypical implementation have shown very good success rates on real-world ontologies.
The origins of interest in forgetting can be traced back to the work of Boole on
propositional variable elimination and the seminal work of Ackermann [
Because forgetting is an inherently difficult problem — it is much harder than
standard reasoning (satisfiability testing) — and very few logics are known to be complete
for forgetting (or have the uniform interpolation property),1 there has been insufficient
research on the topic (in particular on the topic of role forgetting), and few forgetting
1 Konev et al. [
E L, and the existence of forgetting a concept (role) symbol is undecidable for ALC.
tools are available. Recent work has developed practical methods for computing
uniform interpolants for ontologies defined in expressive OWL language dialects [
An alternative approach that performs both concept and role forgetting is described,
automated and evaluated in [
In this paper, we follow an Ackermann-based approach to forgetting, and present a practical method for semantic role forgetting in expressive description logics not considered so far. In particular, the method accommodates ontologies expressible in the description logic ALCOQH and the extension with the universal role O. The extended expressivity enriches the target language, making it expressive enough to represent the forgetting solution which otherwise would have been lost. For example, the solution of forgetting the role symbol frg from the ontology fA1 v 2r:B1; A2 v 1r:B2g is fA1 v 2O:B1; A1 u A2 v 1O:(B1 u :B2)g, whereas in a description logic without the universal role, the uniform interpolant is f>g, which is weaker. Being based on non-trivial generalizations of Ackermann’s Lemma, the method is the only approach so far for forgetting role symbols in description logics with qualified number restrictions. The method is goal-oriented and incremental. It always terminates and is sound in the sense that the forgetting solution is equivalent to the original ontology up to the symbols that have been forgotten, possibly with new concept definer symbols. Our method is nearly role forgetting complete for ALCOQH(O)-ontologies, and we characterize cases where the method is complete. Only problematic are cases where forgetting a role symbol would require the combinations of certain cardinality constraints and role inclusions. Despite the inherent difficulty of forgetting for this level of expressivity, performance results of an evaluation with a prototypical implementation have shown very good success rates on real-world ontologies. 2
ALCOQH(O) and Other Basic Notions Let NC, NR and NO be countably infinite and pairwise disjoint sets of concept symbols, role symbols and individual symbols (nominals), respectively. Roles in ALCOQH(O) can be any role symbol r 2 NR or the universal role O. Concepts in ALCOQH(O) have one of the following forms: a j > j A j :C j C u D j C t D j mR:C j nR:C, where a 2 NO, A 2 NC, C and D are any concepts, R is any role, and m 1 and n 0 are natural numbers. Additional concepts and roles are defined as abbreviations: ? = :>, M= :O, 9R:C = 1R:C, 8R:C = 0R::C, : mR:C = nR:C and : nR:C = mR:C with n = m 1. Concepts of the form mR:C and nR:C are referred to as qualified number restrictions (or number restrictions for short), which allow one to specify cardinality constraints on roles. We assume w.l.o.g. that concepts and roles are equivalent relative to associativity and commutativity of u and t, > and O are units w.r.t. u, and : is an involution.
An ALCOQH(O)-ontology is mostly assumed to be composed of a TBox, an RBox and an ABox. A TBox T is a finite set of concept axioms of the form C v D (concept inclusion), where C and D are concepts. An RBox R is a finite set of role axioms of the form r v s (role inclusion), where r; s 2 NR. We define C D and r s as abbreviations for the pair of C v D and D v C and the pair of r v s and s v r, respectively. An ABox A is a finite set of concept assertions of the form C(a) and role assertions of the form R(a; b), where a; b 2 NO, C is a concept, and R is a role. In a description logic with nominals, ABox assertions can be equivalently expressed as TBox axioms, namely, C(a) as a v C and R(a; b) as a v 9R:b. Hence, in this paper, we assume w.l.o.g. that an ontology contains only TBox and RBox axioms.
The semantics of ALCOQH(O) is defined as usual. A concept axiom C v D is true in an interpretation I, and we write I j= C v D, iff CI DI . A role axiom r v s is true in an interpretation I, and we write I j= r v s, iff rI sI . I is a model of an ontology O iff every axiom in O is true in I. In this case we write I j= O.
Our method works with TBox and RBox axioms in clausal normal form. We assume w.l.o.g. that a TBox literal is a concept of the form a, :a, A, :A, mR:C or nR:C, where a 2 NO, A 2 NC, m 1 and n 0 are natural numbers, C is any concept, and R is any role. A TBox clause is a disjunction of a finite number of TBox literals. An RBox clause is a disjunction of a role symbol and a negated role symbol. TBox and RBox clauses are obtained by clausification of TBox and RBox axioms, where in the latter case role negation is introduced. This is done for consistency in presentation, replacing role inclusion by disjunction as the main operator. Nominals are treated as regular concept symbols in our method, because we are only concerned with role forgetting in this paper. An axiom (clause) that contains a designated (concept or role) symbol S is called an S-axiom (S-clause). An occurrence of S is assumed to be positive (negative) in an S-axiom (S-clause) if it is under an even (odd) number of explicit and implicit negations. For instance, r is assumed to be positive in mr:A and s v r, and negative in nr:A and r v s. A set N of axioms (clauses) is assumed to be positive (negative) w.r.t. S if every occurrence of S in N is positive (negative). 3
Forgetting can be formalized in two ways that are closely related: one is analogous to
model inseparability (i.e., a semantic notion based on model-conservative extensions;
see e.g. [
Our notion of forgetting is a semantic notion. By sigC(X) and sigR(X) we denote the sets of respectively the concept and role symbols occurring in X (excluding nominals), where X ranges over axioms, clauses, sets of axioms, and sets of clauses. Let r 2 NR be any role symbol, and let I and I0 be any interpretations. We say I and I0 are equivalent up to r, or r-equivalent, if I and I0 coincide but differ possibly in the interpretations of r. More generally, I and I0 are equivalent up to a set of role symbols, or -equivalent, if I and I0 coincide but differ possibly in the interpretations of the symbols in . This can be understood as follows: (i) I and I0 have the same domain, i.e., I = I0 , and interpret every concept symbol and every individual symbol identically, i.e., AI = AI0 for every A 2 NC and aI = aI0 for every a 2 NO; (ii) for every role symbol r 2 NR not in , rI = rI0 .
tology and let be a subset of sigR(O). An ontology O0 is a solution of forgetting from O, iff the following conditions hold: (i) sigR(O0) sigR(O)n , and (ii) for any interpretation I: I j= O0 iff I0 j= O, for some interpretation I0 -equivalent to I.
It follows from this that: (i) the original ontology O and the forgetting solution O0 are equivalent up to (the interpretations of) the symbols in . Also (ii) forgetting solutions are unique up to equivalence, that is, if both O0 and O00 are solutions of forgetting from O, then they are logically equivalent. In this paper, is always assumed to be a set of symbols to be forgotten. The symbol in under current consideration for forgetting is referred to as the pivot in our method. An axiom (clause) that contains an occurrence of the pivot is referred to as a pivot-axiom (pivot-clause).
Given an ontology O and a set of concept and role symbols, computing a solution
of forgetting from O can be reduced to the problem of eliminating single symbols
in . This can be based on the use of a monotonicity property found in [
tains axioms 1 v S ; :::; n v S , where S 2 NC (or S 2 NR), and the i (1 i n) are concepts (or roles) that do not contain S . If Onf 1 v S ; :::; n v S g is negative w.r.t. S , then OS1t:::t n is a solution of forgetting fS g from O (i.e., Conditions (i) and (ii) of Definition 1 hold), where OS1t:::t n denotes the ontology obtained from O by substituting 1 t ::: t n for every occurrence of S in O.
The idea of this theorem is based on a notion of ‘substitution’, which can informally yet intuitively be understood as follows: given an ontology O with S 2 sigC(O) (or S 2 sigR(O)) being the pivot, if there exists a concept (or a role) such that S 62 sig( ) and defines S w.r.t. O, then we can substitute this definition for every occurrence of S in O (S is thus eliminated from O). This theorem also holds, when the inclusions are reversed, i.e., S v 1; :::; S v n, and the polarity of S in the rest of O is switched, i.e., OnfS v 1; :::; S v ng is positive w.r.t. S .
A crucial task in Ackermann-based approaches, therefore, is to find a definition of the pivot w.r.t. the present ontology, that is, to reformulate all pivot-axioms with positive occurrences of the pivot in the form v S (or dually, with negative occurrences of the pivot in the form S v ), where S 62 sig( ). In the context of this paper where axioms are represented in clausal form, this means reformulating all pivot-clauses with positive occurrences of the pivot in the form : t S (or dually, with negative occurrences of the pivot in the form :S t ), where S 62 sig( ).
In the case of concept forgetting, a concept symbol (or a negated concept symbol)
deep inside a clause could be moved outward by using Galois connections between 8r
and 8r (e.g., a TBox clause :At8r:S can be equivalently rewritten as (8r ::A)tS,
where r denotes the inverse of r), or by exploiting the idea of Skolemization (e.g.,
an ABox clause :a t 9r::S can be equivalently rewritten as :a t 9r:b and :b t :S,
where b is a fresh nominal). This is explained in detail in the work of [
In the case of role forgetting, since every role symbol that occurs in a TBox clause is always preceded by a role restriction operator, it is not obvious how to reformulate the TBox pivot-clauses. Thus a direct approach based on Ackermann’s Lemma does not seem feasible for role forgetting in ontologies with TBoxes.
How then to do role forgetting? For the translation of ontologies in first-order logic,
there are no such obstacles. We could apply Ackermann’s Lemma for first-order logic
(e.g., as in the DLS algorithm [
In this section, we introduce our approach to eliminating a single role symbol from a set of TBox and RBox clauses expressible in ALCOQH(O). It is a direct approach based on non-trivial generalizations of Ackermann’s Lemma. The approach has two key ingredients: (i) transformation of the pivot-clauses into reduced form, and (ii) a set of Ackermann rules. The Ackermann rules reflect the generalizations of Ackermann’s Lemma and allow a role symbol to be eliminated from a set of clauses in reduced form. Definition 2 (Reduced Form). For r 2 NR the pivot, a TBox pivot-clause is in reduced form if it has the form E t mr:F or E t nr:F , where E and F are concepts that do not contain r, and m 1 and n 0 are natural numbers. An RBox pivot-clause is in reduced form if it has the form :S t r or S t :r, where S 2 NR and S 6= r. A set N of clauses is in reduced form if all pivot-clauses in N are in reduced form.
The reduced forms incorporate all basic forms of TBox and RBox clauses in which a role symbol could occur. Transforming a TBox pivot-clause into reduced form is not always possible however, unless definer symbols are introduced. Definer symbols Ackermann I
z
N ; C1 t Ackermann II
PR+(r) x1r:D1; : :}:|; Cm t
xmr:Dm{; PT (r)
PR(r) zE1 t y1r:F1; : }:|:; En t ynr:Fn{; tz1 t :r; :}:|: ; tw t :r{ N ; BLOCK(PT+(r); E1 t y1r:F1); :::; BLOCK(PT+(r); En t ynr:Fn);
BLOCK(PT+(r); t1 t :r); :::; BLOCK(PT+(r); tw t :r) Ackermann III N ; z:s1 t r; :}:|: ; :sv t r{; zE1 t
y1r:F1; : }:|:; En t ynr:Fn{; tz1 t :r; :}:|: ; tw t :r{ N ; BLOCK(PR+(r); E1 t y1r:F1); :::; BLOCK(PR+(r); En t ynr:Fn);
BLOCK(PR+(r); t1 t :r); :::; BLOCK(PR+(r); tw t :r)
PT (r)
PR(r) z N ; C1 t
PT+(r) x1r:D1; : :}:|; Cm t
PT ;0(r) xmr:Dm{; z:s1 t r; :}:|: ; :sv t r;
{ PR+(r) 6n.thB-tLieOrCBKL(OPCTK;0:(frC);i :tsEk1ttr): :d:etnoEtens tthe set: fE1 t 0sk:F1; : : : ; En t 0sk:Fng.
xiO:(Di u :F1 u : : : u :Fn)g 7. BLOCK(PR(r); Ci t xir:Di) denotes the set: fCi t xit1:Di; : : : ; Ci t xitw:Dig. 8. BLOCK(PR(r); :sk t r) denotes the set: ft1 t :sk; : : : ; tw t :skg.
Fig. 1. Ackermann rules for eliminating the pivot r 2 NR from a set of clauses in reduced form
are auxiliary concept symbols that do not occur in the present ontology [
Theorem 2. Using definer introduction as described in [
Let N be a set of TBox and RBox clauses exhibiting all different reduced forms, for r 2 sigR(N ) the pivot. We refer to the clauses of the form C t mr:D and the form C t nr:D as positive TBox premises and negative TBox premises of the Ackermann rules, respectively. We refer to the clauses of the form :S t r and the form S t :r as positive RBox premises and negative RBox premises of the Ackermann rules, respectively. By PT+(r) and PT (r) we denote respectively the sets of positive TBox premises and negative TBox premises. By PR+(r) and PR(r) we denote respectively the sets of positive RBox premises and negative RBox premises. By P+(r) and P (r) we denote respectively the union of PT+(r) and PR+(r), and the union of PT (r) and PR(r).
The Ackermann rules, shown in Figure 1, are based on an idea of ‘combination’. Specifically, the idea is to combine all positive premises P+(r) with every negative premise (r) in P (r) (or dually, to combine all negative premises P (r) with every positive premise (r) in P+(r)). The result is a finite set of clauses, denoted by BLOCK(P+(r); (r)) (BLOCK(P (r); (r))). It is observed that the result obtained from combining P+(r) with a negative premise is always identical to the union of the results obtained from combining respectively PT+(r) and PR+(r) with that premise (the dual also holds). We therefore treat every combination of P+(r) with a negative premise as two separate combinations in our Ackermann rules (same for the dual), so that it can be understood better from which premises a resulting BLOCK of clauses is obtained.
For different PT+(r), PR+(r), PT (r), PR(r) and (r), the combination is performed as 8 different cases (see Figure 1). For most of these cases, the idea is analogous to that of Ackermann’s Lemma (and its dual), where the pivot is eliminated by substituting its definition found w.r.t. the present premises for every occurrence of the pivot in these premises. Only for Cases 1 and 5, the combination has a different flavor; their idea is illustrated with two concrete examples.
Case 1: Combining PT+(r) with a negative TBox premise in PT (r), e.g., Ej t yj r:Fj (1 j n), yields a set of TBox clauses, denoted by BLOCK(PT+(r); Ej t yj r:Fj ). Example 1. Combining PT+(r) = fA1 t 2r:B1; A2 t 1r:B2g with fA t 1r:Bg yields a set BLOCK(PT+(r); A t 1r:B) that contains the following subsets of clauses: Ground BLOCK: fA1 t 2O:B1; A2 t 1O:B2g 1st-tier BLOCK: fA t A1 t 1O:(B1 u :B)g 2nd-tier BLOCK: fA t A1 t A2 t 1O:(B1 u B2) t 2O:((B1 t B2) u :B). Case 5: Combining PT ;0(r) with a positive TBox premise in PT+(r), e.g., Ci t (1 i m), yields a set of TBox clauses, denoted by BLOCK(PT ;0(r); Cit In this case, PT ;0(r) denotes the set of negative TBox premises of the form E t (i.e., the cardinality constraints are 0).
xir:Di xir:Di).
0r:F ;0(r) = fA1 t 0r:B1; A2 t 0r:B2g with fA t 2r:Bg Example 2. Combining ;P0(Tr); At 2r:B) that contains the following subsets of clauses: yields a set BLOCK(PT Ground BLOCK: fA t 2O:Bg 1st-tier BLOCK: fA t A1 t 2nd-tier BLOCK: fA t A1 t A2 t 2O:(B u :B1 u :B2)g. 2O:(B u :B1)g
How are the Ackermann rules used? For a set N of clauses in reduced form, depending on which kinds of premises the set N contains, we apply different Ackermann rules (to the premises to eliminate the pivot). Specifically, if N contains only positive TBox premises, as well as negative premises, we apply the Ackermann I rule. If N contains only positive RBox premises, as well as negative premises, we apply the Ackermann II rule. If N contains both positive TBox and RBox premises, as well as negative premises, we apply the Ackermann III rule. Note that there is a gap in the scope of the rules in the Ackermann III rule; it is applicable only to the cases where all negative TBox premises (if they are present in N ) are of the form E t 0r:F (i.e., the cardinality constraints are 0). If N contains only positive (negative) premises, we substitute the universal role (the negated universal role) for every occurrence of the pivot in N . Theorem 3. Let I be any ALCOQH(O)-interpretation. For r 2 NR the pivot, when an Ackermann rule is applicable, the conclusion of the rule is true in I iff for some interpretation I0 r-equivalent to I, the premises are true in I0.
This implies that the conclusion of an Ackermann rule is a solution of forgetting the pivot from the premises of the rule. 5
Given an ontology O of axioms and a set of role symbols to be forgotten, the forgetting process in our method comprises three main phases: (i) the conversion of O into a set N of clauses (the first phase), (ii) the -symbol elimination phase (the central phase), and (iii) the definer elimination phase (the final phase). It is assumed that as soon as a forgetting solution is computed, the remaining phases are skipped.
The first phase: The first phase of the forgetting process internalizes all ABox assertions in O (if they are present in O) into TBox axioms, and then transforms O into a set N of clauses using standard clausal form transformations.
The central phase: Central to the forgetting process is the -symbol elimination phase, which is an iteration of several rounds in which the elimination of -symbols is attempted. Specifically, the method attempts to eliminate the -symbols one by one using the approach as described in the previous section. In each elimination round, the method performs two steps. The first step transforms every TBox pivot-clause (not in reduced form) into reduced form, so that one of the Ackermann rules can be applied. The second step then applies the Ackermann rule to the pivot-clauses to eliminate the pivot. Upon the intermediate result being returned at the end of each round, the method repeats the same steps in the next round for the elimination of the remaining symbols in (if necessary). If a -symbol has been found ineliminable from the present ontology (i.e., none of the Ackermann rules is applicable to the current reduced form), the method skips the current round and attempts to eliminate another symbol in .
The final phase: To facilitate the transformation of TBox pivot-clauses (not in
reduced form) into reduced form, definer symbols might have been introduced during the
elimination rounds. The final phase of the forgetting process attempts to eliminate these
definer symbols by using Ackermann-based rules for concept forgetting; for details
see [
What the method returns as output at the end of the forgetting process is a finite set O0 of clauses. If O0 does not contain any symbols in , then the method was successful in computing a solution of forgetting from O. The following theorem states termination and soundness of the method.
Theorem 4. For any ALCOQH(O)-ontology O and any set sigR(O) of role symbols to be forgotten, the method always terminates and returns a finite set O0 of clauses. (i) If O0 does not contain any symbols in or any newly-introduced definer symbols, then O0 is a solution of forgetting from O (i.e., O0 is equivalent to the original ontology O up to the symbols in ). (ii) If O0 does not contain any symbols in but it contains newly-introduced definer symbols, then O0 is a solution of forgetting from O in an extended language (and O and O0 are equivalent up to the symbols in , as well as the newly-introduced definer symbols present in O0).
The method may return a finite set O0 of clauses that still contains some -symbols. In this case, the method was not successful. This is because there is a gap in the scope of the rules in the Ackermann III rule, as mentioned before Theorem 3. Theorem 5. Given an ALCOQH(O)-ontology O in clausal form and a subset of sigR(O), our method is guaranteed to compute a solution of forgetting from O, possibly with concept definer symbols, iff any one of the following conditions holds for each r 2 : (i) O does not contain any RBox axioms of the form :S t r for S 6= r; (ii) O does not contain any TBox axioms with number restrictions of the form mr:D for m 1; or (iii) O does not contain any TBox axioms with number restrictions of the form nr:D for n 1.
An explanation of Case (ii) is the following: let O be an ALCOQH(O)-ontology in clausal form, and let be a subset of sigR(O). For r 2 the pivot, if O does not contain any TBox axioms with number restrictions of the form mr:D for m 1, then there will be no positive TBox premises occurring in O (when O is transformed into reduced form). O is thus in the form suitable for application of the Ackermann II rule. Explanations of Cases (i) and (iii) are similar, i.e., O of Cases (i) and (iii) in reduced form are suitable for application of the Ackermann I and III rules, respectively. 6
To gain insight into the practical applicability of the method, we implemented a prototype in Java using the OWL-API, and evaluated it on two corpora of slightly adjusted real-world ontologies from the NCBO BioPortal repository.2 The experiments were run 2 http://bioportal.bioontology.org/ on a desktop computer with an Intelr CoreTM i7-4790 processor, four cores running at up to 3.60 GHz and 8 GB of DDR3-1600 MHz RAM.
The corpora used for our experiments were constructed as follows. First, we selected from the NCBO BioPortal repository ontologies containing both number restrictions and role inclusions. Then, we filtered out those containing less than 40 role symbols (because they were less challenging). Consequently, five ontologies stood out from the repository (see Figure 2 for their profiles). We further adjusted these ontologies to the language of ALCOQH (i.e., none of them included the universal role O). This was done by removing those axioms not expressible in ALCOQH and using simple simulations. For example, an exact number restriction =1r:D was simulated by ( 1r:D)u( 1r:D), and a functional role func(r) was simulated by 1r:>. In this way we obtained a corpus (Corpus I) of five ALCOQH-ontologies. By removing all role inclusions in each of the ontologies in Corpus I, we obtained another corpus (Corpus II) that contained five ALCOQ-ontologies. Using Corpora I and II as test data sets for our experiments, we considered how the presence of role inclusions affected the results of role forgetting, in particular, the success rates.
To fit in with different real-world use, we evaluated the performance of forgetting different numbers of role symbols from each ontology. In particular, we forgot 30% (i.e., a small number) and 70% (i.e., a large number) of role symbols in the signature of each ontology. The symbols to be forgotten were randomly chosen. We ran the experiments 50 times on each ontology and averaged the results to verify the accuracy of our findings. A timeout of 100 seconds was imposed on each run of the experiment.
The results are shown in Figure 3, which is rather revealing in several ways. The most encouraging result was that our prototype was successful (i.e., forgot all symbols in ) in all test cases (within a short period of time) except in the case of SDO, despite role inclusions being present in them. This was unexpected, but there are obvious explanations (for the 100% success rate cases): inspection revealed that these ontologies did not contain axioms with number restrictions of the form nS:D for n 1, and the likelihood of -symbols occurring positively in the RBox axioms was very low. What was as expected was that definer symbols were not introduced in the test ontologies (as most real-world ontologies were by design flat and therefore already in reduced form). This gave us best benefits of using our Ackermann-based approach. Because of the nature of the Ackermann III and V rules, forgetting a role symbol could lead to growth of clauses in the forgetting solution, which was however modest (see the G.C. column in Figure 3) compared to the theoretical worst case (i.e., 2n 1 for n the cardinality of PT+). In the case of SDO the ‘hasPart’ role occurred positively in more than 50 different TBox clauses in reduced form. This means that if ‘hasPart’ was chosen as one of the -symbols to be forgotten, then there were more than 50 positive TBox premises in the ontology SDO in reduced form (i.e., n 50), which led to a blow-up of clauses in the forgetting solution (i.e., 250 1 clauses). Indeed, the failures on SDO were due to space explosion caused by the high frequency of the ‘hasPart’ role. We found that without this role in , the success rate was 100%. 7
In this paper, we have presented a practical method of semantic role forgetting for ontologies expressible in the description logic ALCOQH(O). The method is the only approach so far for forgetting role symbols in description logics with number restrictions. This is very useful from the perspective of ontology engineering as it increases the arsenal of tools available to create decompositions and restricted views of ontologies. We have shown that the method is terminating and is sound in the sense that the forgetting solution is equivalent to the original ontology up to the forgotten symbols, sometimes with new concept definer symbols. Although our method is not complete, performance results of an evaluation with a prototypical implementation have shown very good success rates on two corpora of real-world biomedical ontologies.
Though the main focus of this paper has been the problem of role forgetting, (nonnominal) concept forgetting can be reduced to role forgetting by substituting 1r:> for every occurrence of the concept symbol one wants to forget, where r is a fresh role symbol, and then forgetting frg. For example, forgetting the concept symbol fBg from the ontology f:A t 1s:Bg can be reduced to the problem of forgetting the role symbol frg from the ontology f:A t 1s: 1r:>g. Thus our method also provides an incomplete approach to concept forgetting for ALCOQH(O)-ontologies.