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.