=Paper= {{Paper |id=Vol-1879/paper4 |storemode=property |title=Role Forgetting for ALCOQH(universal role)-Ontologies Using an Ackermann-Based Approach |pdfUrl=https://ceur-ws.org/Vol-1879/paper4.pdf |volume=Vol-1879 |authors=Yizheng Zhao,Renate A. Schmidt |dblpUrl=https://dblp.org/rec/conf/dlog/ZhaoS17 }} ==Role Forgetting for ALCOQH(universal role)-Ontologies Using an Ackermann-Based Approach== https://ceur-ws.org/Vol-1879/paper4.pdf
          Role Forgetting for ALCOQH(O)-Ontologies
              Using an Ackermann-Based Approach

                             Yizheng Zhao and Renate A. Schmidt

                 School of Computer Science, The University of Manchester, UK
                {yizheng.zhao,renate.schmidt}@manchester.ac.uk


          Abstract. 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 for-
          getting 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 forgot-
          ten symbols, possibly with new concept definer symbols. Despite our method not
          being complete, performance results of an evaluation with a prototypical imple-
          mentation have shown very good success rates on real-world ontologies.


1      Introduction

The origins of interest in forgetting can be traced back to the work of Boole on proposi-
tional variable elimination and the seminal work of Ackermann [1] who recognized that
the problem amounts to the elimination of existential second-order quantifiers. In logic
the problem has been studied as the (dual) uniform interpolation problem [29, 5, 10], a
notion related to the Craig interpolation problem, but stronger. In computer science the
importance of forgetting can be found in the knowledge representation literature [21,
20, 6], specification refinement literature [2] and the area of description logic-based
ontology engineering [31, 32, 30, 11, 13, 12, 24, 23, 9, 22, 25, 3]. In ontology-based in-
formation processing, forgetting allows users to focus on specific parts of ontologies in
order to create decompositions and restricted views for in depth analysis or sharing with
other users. Forgetting is also useful for information hiding, explanation generation, and
ontology debugging and repair.
    Because forgetting is an inherently difficult problem — it is much harder than stan-
dard 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. [12] have shown that the solution of forgetting does not always exist for ALC and
     EL, and the existence of forgetting a concept (role) symbol is undecidable for ALC.
tools are available. Recent work has developed practical methods for computing uni-
form interpolants for ontologies defined in expressive OWL language dialects [15, 16,
18]. These methods, which are saturation approaches based on resolution, can eliminate
both concept and role symbols and can handle ontologies specified in description logics
from ALC to ALCH and SIF. The methods have been extended to SHQ for concept
forgetting in [17]. While most of this work is focused on TBox and RBox uniform in-
terpolation, practical methods for uniform interpolation for description logics ALC and
SHI with ABoxes are described in [19, 14].
    An alternative approach that performs both concept and role forgetting is described,
automated and evaluated in [34]. This approach is a semantic approach which accom-
modates ontologies expressible in description logics with nominals, role inverse, role
inclusions, role conjunction and the universal role. The foundation for this approach is
an adaptation of a monotonicity property called Ackermann’s Lemma [1], which also
provides the foundation for approaches to second-order quantifier elimination [7, 26, 8]
and modal correspondence theory [28, 4, 27].
    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 con-
sidered 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 {r} from the ontology {A1 v ≥2r.B1 , A2 v ≤1r.B2 } is
{A1 v ≥2O.B1 , A1 u A2 v ≥1O.(B1 u ¬B2 )}, whereas in a description logic with-
out the universal role, the uniform interpolant is {>}, 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 sym-
bols 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, per-
formance 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 ∈ NR or the universal role O. Concepts in ALCOQH(O)
have one of the following forms: a | > | A | ¬C | C u D | C t D | ≥mR.C | ≤nR.C,
where a ∈ NO , A ∈ 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, ∃R.C = ≥1R.C, ∀R.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 ∈ 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 ∈ 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 ∃R.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 |= C v D, iff C I ⊆ DI . A role axiom
r v s is true in an interpretation I, and we write I |= 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 |= 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 ∈ NO , A ∈ 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, replac-
ing 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, Ackermann’s Lemma, Obstacles to Role Forgetting

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. [12]), which preserves equivalence up to certain signatures (i.e., parameterized
equivalence), and the other is via uniform interpolation (i.e., a syntactic notion based on
deductive-conservative extensions; see e.g. [29]), which preserves logical consequences
up to certain signatures; see [3] a survey for their interrelation.
    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 nom-
inals), where X ranges over axioms, clauses, sets of axioms, and sets of clauses. Let
r ∈ NR be any role symbol, and let I and I 0 be any interpretations. We say I and
I 0 are equivalent up to r, or r-equivalent, if I and I 0 coincide but differ possibly in
the interpretations of r. More generally, I and I 0 are equivalent up to a set Σ of role
symbols, or Σ-equivalent, if I and I 0 coincide but differ possibly in the interpretations
of the symbols in Σ. This can be understood as follows: (i) I and I 0 have the same do-
                      0
main, i.e., ∆I = ∆I , and interpret every concept symbol and every individual symbol
                           0                                 0
identically, i.e., AI = AI for every A ∈ NC and aI = aI for every a ∈ NO ; (ii) for
                                              0
every role symbol r ∈ NR not in Σ, rI = rI .

Definition 1 (Role Forgetting for ALCOQH(O)). Let O be an ALCOQH(O) on-
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)\Σ, and (ii) for any
interpretation I: I |= O0 iff I 0 |= O, for some interpretation I 0 Σ-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 solu-
tions 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 [1], referred to
as Ackermann’s Lemma. For ontologies, Ackermann’s Lemma can be formulated as the
following theorem. The proof is an easy adaptation of Ackermann’s original result [8].

Theorem 1 (Ackermann’s Lemma for Ontologies). Let O be an ontology that con-
tains axioms α1 v S, ..., αn v S, where S ∈ NC (or S ∈ NR ), and the αi (1 ≤ i ≤ n)
are concepts (or roles) that do not contain S. If O\{α1 v S, ..., αn v S} is negative
w.r.t. S, then OαS1 t...tαn is a solution of forgetting {S} from O (i.e., Conditions (i) and
(ii) of Definition 1 hold), where OαS1 t...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 ∈ sigC (O) (or
S ∈ sigR (O)) being the pivot, if there exists a concept (or a role) α such that S 6∈ 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., O\{S v α1 , ..., S v αn } 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 6∈ 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 6∈ 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 ∀r
and ∀r− (e.g., a TBox clause ¬At∀r.S can be equivalently rewritten as (∀r− .¬A)tS,
where r− denotes the inverse of r), or by exploiting the idea of Skolemization (e.g.,
an ABox clause ¬a t ∃r.¬S can be equivalently rewritten as ¬a t ∃r.b and ¬b t ¬S,
where b is a fresh nominal). This is explained in detail in the work of [4, 27, 33, 34].
    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 D LS algorithm [7]) to eliminate a single role symbol. Such an indi-
rect approach requires suitable back-translation however, which is absent at present
for expressive description logics. Translating first-order formulas back into equivalent
description logic expressions is not straightforward, in particular when number restric-
tions are present in the target language. For example, the solution of forgetting the role
symbol {r} from {A1 t ≥2r.B1 , A2 t ≤1r.B2 } in first-order logic is the set:

     {∀x(A1 (x) ∨ B1 (f1 (x))), ∀x(A1 (x) ∨ B1 (f2 (x))), ∀x(A1 (x) ∨ f1 (x) 6≈ f2 (x)),
       ∀x(A1 (x) ∨ A2 (x) ∨ ¬B2 (f1 (x)) ∨ ¬B2 (f2 (x)))},

where f1 (x) and f2 (x) are Skolem terms, and f1 (x) 6≈ f2 (x) is an inequality. Because
of the presence of the Skolem terms and the inequality, it is not clear whether this
solution can be expressed equivalently in a description logic.


4   Our Approach to Eliminating A Single Role Symbol
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 ∈ 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 ∈ 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
                                   P + (r)
                                   T
                 z                  }|               {
             N , C1 t ≥x1 r.D1 , . . . , Cm t ≥xm r.Dm ,
                              T
                                 P − (r)                            P − (r)
                                                               R
             z                 }|                 { z          }|           {
             E1 t ≤y1 r.F1 , . . . , En t ≤yn r.Fn , t1 t ¬r, . . . , tw t ¬r
    N , B LOCK(PT+ (r), E1 t ≤y1 r.F1 ), ..., B LOCK(PT+ (r), En t ≤yn r.Fn ),
                        B LOCK(PT+ (r), t1 t ¬r), ..., B LOCK(PT+ (r), tw t ¬r)
    Ackermann II
                                                            −
                 P + (r)                                   PT (r)
                                                                                     R
                                                                                        P − (r)
                 R
        z         }|            { z                  }|                { z           }|          {
    N , ¬s1 t r, . . . , ¬sv t r, E1 t ≤y1 r.F1 , . . . , En t ≤yn r.Fn , t1 t ¬r, . . . , tw t ¬r
                          +                                      +
        N , B LOCK(PR       (r), E1 t ≤y1 r.F1 ), ..., B LOCK(PR   (r), En t ≤yn r.Fn ),
                                           +                                 +
                                 B LOCK(PR (r), t1 t ¬r), ..., B LOCK(PR       (r), tw t ¬r)
    Ackermann III
                                   P + (r)
                                   T                                    P + (r)
                                                                  R
                 z                  }|               { z           }|           {
             N , C1 t ≥x1 r.D1 , . . . , Cm t ≥xm r.Dm , ¬s1 t r, . . . , ¬sv t r,
                                               −,0
                                        T
                                           P         (r)
                                                                        R
                                                                              P − (r)
                        z                 }|               { z           }|         {
                        E1 t ≤0r.F1 , . . . , En t ≤0r.Fn , t1 t ¬r, . . . , tw t ¬r
    N , B LOCK(PT−,0 (r), C1 t ≥x1 r.D1 ), ..., B LOCK(PT−,0 (r), Cm t ≥xm r.Dm ),
        B LOCK(PT−,0 (r), ¬s1 t r), ..., B LOCK(PT−,0 (r)), ¬sv t r),
                    −                                         −
           B LOCK(PR  (r), C1 t ≥x1 r.D1 ), ..., B LOCK(PR       (r)), Cm t ≥xm r.Dm ),
                                           −                                −
                             B LOCK(PR       (r), ¬s1 t r), ..., B LOCK(PR    (r)), ¬sv t r)
Notation in Ackermann rules (1 ≤ i ≤ m, 1 ≤ j ≤ n, 1 ≤ k ≤ v, 1 ≤ l ≤ w):
1. B LOCK(PT+ (r), Ej t ≤yj r.Fj ) denotes the union of following sets:
Ground B LOCK: {C  S1 t ≥x1 O.D1 , . . . , Cm t ≥xm O.Dm }
1st-tier B LOCK:       {Ej t Ci t ≥(xi − yj )O.(Di u ¬Fj )} for any i such that xi > yj
                 1≤i≤m
                      S
2nd-tier B LOCK:            {Ej t Ci1 t Ci2 t ≥xO.(Di1 u Di2 ) t ≥(xi1 + xi2 − yj − (x −
                   1≤i1  yj ,
where xmin denotes the minimum of xi1 , xi2 and xi1 + xi2 − yj .
      ...
mth-tier B LOCK: {Ej tC1 t. . .tCm t≥xO.(D1 u. . .uDm )t≥(x1 +. . .+xm −yj −(x−
1))O.((D1 t. . .tDm )u¬Fj )t. . .t≥1O.((D1 t. . .tDm )u¬Fj ) | x ∈ {1, . . . , xmin }} if
x1 + . . . + xm ≥ yj , where xmin denotes the minimum of x1 , . . . , xm and x1 + ... + xm − yj .
2. B LOCK(PT+ (r), tl t ¬r) denotes the set: {C1 t ≥x1 tl .D1 , . . . , Cm t ≥xm tl .Dm }.
               +
3. B LOCK(PR     (r), Ej t ≤yj r.Fj ) denotes the set: {Ej t ≤yj s1 .Fj , . . . , Ej t ≤yj sv .Fj }.
               +
4. B LOCK(PR     (r), tl t ¬r) denotes the set: {¬s1 t tl , . . . , ¬sv t tl }.
5. B LOCK(PT−,0 (r), Ci t ≥xi r.Di ) denotes the union of following sets:
Ground B LOCK: {C   Si t ≥xi O.Di }
1st-tier B LOCK:          {Ci t Ej t ≥xi O.(Di u ¬Fj )}
                  1≤j≤n
                         S
2nd-tier B LOCK:               {Ci t Ej1 t Ej2 t ≥xi O.(Di u ¬Fj1 u ¬Fj2 )}
                   1≤j1 . 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 experi-
ments 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 ex-
planations (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 na-
ture of the Ackermann III and V rules, forgetting a role symbol could lead to growth of
         Σ (30%)                Corpus I                      Corpus II
         Ontology    D.I.    Time    S.R.    G.C.    D.I.   Time    S.R.      G.C.
           PANDA      0      0.576   100%    0.0%     0     0.571  100%       0.0%
            OPB       0      1.734   100%    4.2%     0     1.695  100%       4.3%
            ROO       0      4.674   100%    0.0%     0     4.339  100%       0.0%
            EPO       0      7.183   100%    7.1%     0     7.171  100%       7.3%
            SDO       0     18.325 71.1%     7.3%     0     17.817 69.4%      7.7%
         Σ (70%)                Corpus I                      Corpus II
           PANDA      0      1.267   100%    0.0%     0     1.252  100%       0.0%
            OPB       0      3.937   100%    6.1%     0     3.869  100%       6.5%
            ROO       0      9.663   100%    0.0%     0     9.602  100%       0.0%
            EPO       0     15.874 100%      8.2%     0     15.389 100%       8.5%
            SDO       0     39.196 32.1%     8.5%     0     38.084 30.9%      8.9%
          D.I. = Definer Introduced, S.R. = Success Rate, G.C. = Growth of Clauses

           Fig. 3. Performance results of forgetting 30% and 70% of role symbols


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   Conclusions
In this paper, we have presented a practical method of semantic role forgetting for on-
tologies expressible in the description logic ALCOQH(O). The method is the only
approach so far for forgetting role symbols in description logics with number restric-
tions. 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 ontolo-
gies. 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, (non-
nominal) 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 {r}. For example, forgetting the concept symbol {B}
from the ontology {¬A t ≥1s.B} can be reduced to the problem of forgetting the role
symbol {r} from the ontology {¬A t ≥1s.≥1r.>}. Thus our method also provides an
incomplete approach to concept forgetting for ALCOQH(O)-ontologies.
References

 1. W. Ackermann. Untersuchungen über das Eliminationsproblem der mathematischen Logik.
    Mathematische Annalen, 110(1):390–413, 1935.
 2. J. Bicarregui, T. Dimitrakos, D. M. Gabbay, and T. S. E. Maibaum. Interpolation in practical
    formal development. Logic Journal of the IGPL, 9(2):231–244, 2001.
 3. E. Botoeva, B. Konev, C. Lutz, V. Ryzhikov, F. Wolter, and M. Zakharyaschev. Inseparability
    and Conservative Extensions of Description Logic Ontologies: A Survey. In Proc. RW’16,
    volume 9885 of LNCS, pages 27–89. Springer, 2016.
 4. W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and completeness
    in modal logic. I. The core algorithm SQEMA. Logical Methods in Comp. Sci., 2(1), 2006.
 5. G. D’Agostino and M. Hollenberg. Logical questions concerning the µ-Calculus: Interpola-
    tion, Lyndon and Los-Tarski. J. Symb. Log., 65(1):310–332, 2000.
 6. J. P. Delgrande and K. Wang. An Approach to Forgetting in Disjunctive Logic Programs that
    Preserves Strong Equivalence. CoRR, abs/1404.7541, 2014.
 7. P. Doherty, W. Łukaszewicz, and A. Szałas. Computing circumscription revisited: A reduc-
    tion algorithm. Journal of Automated Reasoning, 18(3):297–336, 1997.
 8. D. M. Gabbay, R. A. Schmidt, and A. Szałas. Second Order Quantifier Elimination: Foun-
    dations, Computational Aspects and Applications. College Publications, 2008.
 9. B. C. Grau and B. Motik. Reasoning over Ontologies with Hidden Content: The Import-by-
    Query approach. J. Artif. Intell. Res., 45:197–255, 2012.
10. A. Herzig and J. Mengin. Uniform Interpolation by Resolution in Modal Logic. In Proc.
    JELIA’08, volume 5293 of LNCS, pages 219–231. Springer, 2008.
11. B. Konev, C. Lutz, D. Walther, and F. Wolter. Formal Properties of Modularisation. In
    Modular Ontologies: Concepts, Theories and Techniques for Knowledge Modularization,
    volume 5445 of LNCS, pages 25–66. Springer, 2009.
12. B. Konev, C. Lutz, D. Walther, and F. Wolter. Model-theoretic inseparability and modularity
    of description logic ontologies. Artificial Intelligence, 203:66–103, 2013.
13. B. Konev, D. Walther, and F. Wolter. Forgetting and Uniform Interpolation in Large-Scale
    Description Logic Terminologies. In Proc. IJCAI’09, pages 830–835. IJCAI/AAAI Press,
    2009.
14. P. Koopmann. Practical Uniform Interpolation for Expressive Description Logics. PhD
    thesis, The University of Manchester, UK, 2015.
15. P. Koopmann and R. A. Schmidt. Forgetting Concept and Role Symbols in ALCH-
    Ontologies. In Proc. LPAR’13, volume 8312 of LNCS, pages 552–567. Springer, 2013.
16. P. Koopmann and R. A. Schmidt. Uniform Interpolation of ALC-Ontologies Using Fix-
    points. In Proc. FroCos’13, volume 8152 of LNCS, pages 87–102. Springer, 2013.
17. P. Koopmann and R. A. Schmidt. Count and Forget: Uniform Interpolation of SHQ-
    Ontologies. In Proc. IJCAR’14, volume 8562 of LNCS, pages 434–448. Springer, 2014.
18. P. Koopmann and R. A. Schmidt. Saturated-Based Forgetting in the Description Logic SIF.
    In Proc. DL’15, volume 1350 of CEUR Workshop Proc., 2015.
19. 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.
20. J. Lang, P. Liberatore, and P. Marquis. Propositional independence: Formula-variable inde-
    pendence and forgetting. J. Artif. Intell. Res., 18:391–443, 2003.
21. F. Lin and R. Reiter. Forget it! In Proc. AAAI Fall Symposium on Relevance, pages 154–159.
    AAAI Press, 1994.
22. 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.
23. 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.
24. C. Lutz and F. Wolter. Foundations for Uniform Interpolation and Forgetting in Expressive
    Description Logics. In Proc. IJCAI’11, pages 989–995. IJCAI/AAAI Press, 2011.
25. N. Nikitina and S. Rudolph. (Non-)Succinctness of uniform interpolants of general termi-
    nologies in the description logic EL. Artificial Intelligence, 215:120–140, 2014.
26. A. Nonnengart and A. Szałas. A fixpoint approach to second-order quantifier elimination
    with applications to correspondence theory. In Logic at Work: Essays Dedicated to the
    Memory of Helena Rasiowa, pages 307–328. Springer, 1999.
27. R. A. Schmidt. The Ackermann approach for modal logic, correspondence theory and
    second-order reduction. Journal of Applied Logic, 10(1):52–74, 2012.
28. A. Szałas. On the correspondence between modal and classical logic: An automated ap-
    proach. Journal of Logic and Computation, 3:605–620, 1993.
29. A. Visser. Bisimulations, Model Descriptions and Propositional Quantifiers. Logic Group
    Preprint Series. Department of Philosophy, Utrecht Univ., 1996.
30. 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.
31. Z. Wang, K. Wang, R. W. Topor, and J. Z. Pan. Forgetting Concepts in DL-Lite. In Proc.
    ESWC’08, volume 5021 of LNCS, pages 245–257. Springer, 2008.
32. Z. Wang, K. Wang, R. W. Topor, and J. Z. Pan. Forgetting for knowledge bases in DL-Lite.
    Ann. Math. Artif. Intell., 58(1-2):117–151, 2010.
33. Y. Zhao and R. A. Schmidt. Concept Forgetting in ALCOI-Ontologies Using an Ackermann
    Approach. In Proc. ISWC’15, volume 9366 of LNCS, pages 587–602. Springer, 2015.
34. Y. Zhao and R. A. Schmidt. Forgetting Concept and Role Symbols in ALCOIHµ+ (O, u)-
    Ontologies. In Proc. IJCAI’16, pages 1345–1352. IJCAI/AAAI Press, 2016.
35. Y. Zhao and R. A. Schmidt. Role Forgetting for ALCOQH(O)-Ontologies Using an
    Ackermann-Based Approach. In Proc. IJCAI’17, to appear. IJCAI/AAAI Press, 2017.