Fine-Grained Forgetting for the Description Logic ALC Mostafa Sakr, Renate A. Schmidt The University of Manchester, Manchester, UK Abstract Forgetting is an important ontology extraction technique. A variant of forgetting which has received significant attention in the literature is deductive forgetting (or uniform interpolation). While deductive forgetting is attractive as it generates the forgetting view in a language with the same complexity as the language of the original ontology, it is known that with a slightly extended target language using definer symbols more information can be preserved. In this paper, we study deductive forgetting of concept names with the aim of understanding the unpreserved information. We present a system that performs deductive forgetting and produces a set Ξ” of axioms representing the unpreserved information in the forgetting view. Our system allows a new fine-grained ontology extraction process that gives the user the option to enhance the informativeness of the deductive forgetting view by appending to it axioms from Ξ”. 1. Introduction Forgetting is an important ontology extraction technique. It eliminates from an ontology a given subset of its vocabulary. The result is a focused ontology, called forgetting view, which preserves the content of the ontology relative to the non-forgotten vocabulary. Forgetting offers solutions for many applications such as: computing logical difference [1], information hiding [2], abduction [3], resolving conflicts [4], relevance [5, 6, 7], and forgetting actions in planning [8]. A variant of forgetting that has been studied in the literature is deductive forgetting (or uniform interpolation). Given an π’œβ„’π’ž ontology and a forgetting signature, deductive forgetting produces a view of the ontology which preserves only the information expressible in π’œβ„’π’ž over the non-forgetting signature [9, 10, 11]. Deductive forgetting is however not precise, because information expressible with more expressivity may not be preserved. Yet, deductive forgetting remains an appealing variant of forgetting because when performed on π’œβ„’π’ž ontologies, the generated forgetting views are (infinitely) representable in π’œβ„’π’ž, or finitely representable if fixpoint operators are allowed [12, 13]. When a deductive view is computed, the following questions arise: Does the deductive view preserve all information of the non-forgotten vocabulary? If not, what information is not preserved and what does this information represent? Can some of this information be partially preserved, i.e., can a view more informative than the deductive forgetting view be computed? In this paper, we DL 2022: 35th International Workshop on Description Logics, August 7–10, 2022, Haifa, Israel $ Mostafa.Sakr@manchester.ac.uk (M. Sakr); Renate.Schmidt@manchester.ac.uk (R. A. Schmidt)  0000-0003-4296-5831 (M. Sakr); 0000-0002-6673-3333 (R. A. Schmidt) Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) aim to address these questions, gain a better understanding of the information not preserved by deductive forgetting, and provide a practical tool to compute this information. We focus on concept forgetting for ontologies in the description logic π’œβ„’π’ž, the basic logic in the family of expressive description logics [14]. The main contribution is a novel forgetting method. (1) The method converts the input ontology into an intermediate ontology in which the forgetting signature has been eliminated. This intermediate ontology is semantically equivalent to the input ontology with respect to the non-forgotten vocabulary. That is, the reducts of the models of both ontologies to the non- forgotten vocabulary coincide. The intermediate ontology may use foreign concept symbols, or definers, to represent subsets of role successors. (2) The method obtains from the intermediate ontology two sets π’ͺπ‘Ÿπ‘’π‘‘ and Ξ” of axioms. The set π’ͺπ‘Ÿπ‘’π‘‘ approximates the deductive view by allowing the use of foreign symbols. We present a method to eliminate these foreign symbols from π’ͺπ‘Ÿπ‘’π‘‘ and obtain the final deductive view in π’œβ„’π’ž. Complete elimination of the foreign symbols may not however succeed when the deductive view does not exist finitely in π’œβ„’π’ž due to cycles occurring over forgetting symbols. The set Ξ” represents the information difference between the intermediate ontology and π’ͺπ‘Ÿπ‘’π‘‘ . If all foreign symbols are successfully eliminated from π’ͺπ‘Ÿπ‘’π‘‘ , then Ξ” also represents the information difference between the input ontology and the deductive view. Several benefits are obtained from our forgetting method. (1) In two different evaluations an implementation of our forgetting method was compared against the state-of-the-art deductive forgetting tool Lethe [15]. Our implementation was found to be faster than Lethe. Our analysis shows that this improvement can be attributed to a novelty of the language of the intermediate ontology as it allows for avoiding time-consuming operations performed by Lethe. (2) By inspecting the set Ξ”, we now understand the difference between the input ontology and the deductive view as information on the conjunctions of different subsets of role successors. (3) An empty Ξ” indicates that the deductive view coincides semantically with the input ontology with respect to the non-forgotten vocabulary. (4) By incrementing π’ͺπ‘Ÿπ‘’π‘‘ with axioms from Ξ”, our method allows for a fine-grained forgetting framework where views of the original ontology that are more informative than the deductive view can be obtained based on user requirements. All proofs are provided in the long version https://github.com/e73898ms/ FineGrainedForgetting/blob/main/Fine_Grained_Forgetting-Long%20Version-DL22.pdf. 2. History and Related Work Forgetting can be traced back to Boole who referred to it as elimination of the middle terms. In propositional logic, it was studied in relation to relevance, independence, and variable elimina- tion [6, 7]. A variant of forgetting which preserves semantic equivalences is semantic forgetting. In the context of first-order logic (FOL), semantic forgetting was viewed as a second-order quantifier elimination problem [16, 17] finding that the semantic view of a FO theory is not in general expressible in FOL but is always expressible in second-order logic (SOL). A way to view the foreign symbols in the intermediate ontology created by our method is as second-order existentially quantified concept symbols. This is because they are used to represent subsets of role successors whose first-order definition, as we show, cannot be computed in general. Therefore, our intermediate ontology adheres to results in the literature [9, 16], and can be viewed as an approximation to the semantic view of the input ontology. We show that standard reasoning operations can be performed on the intermediate ontology using standard π’œβ„’π’ž reasoning methods. Deductive forgetting was considered in [18] under the name weak forgetting. The proposal in [18] builds on previous work in modal logics which views deductive forgetting as uniform interpolation [19, 20], i.e., forgetting a signature β„± from an ontology π’ͺ is equivalent to computing the uniform interpolant over the remaining vocabulary of π’ͺ after excluding β„±. This allows characterizing the relationship between the original ontology and the deductive view in terms of bisimulation over the non-forgotten symbols [10, 9, 21]. Deductive and semantic forgetting are also closely related to the notions of concept inseparability and model inseparability [22, 23, 24, 25]. Several deductive forgetting methods were proposed in [13, 20, 1]. Deciding the existence of a finitely representable deductive view is 2ExpTime, and its size is, at most, triple exponential in the size of the original ontology [10]. For π’œβ„’π’ž ontologies, the deductive view can be captured, possibly infinitely, in π’œβ„’π’ž. Infinite forgetting views occur when cycles over some forgetting symbols exist [13]. In this case, finite representations may be approximated by fixpoint operators [12, 13, 26, 27] or by using foreign symbols to witness these cycles [13]. The latter representation can be converted to the former [13]. 3. Basic Definitions Let 𝑁𝑐 , π‘π‘Ÿ be two disjoint sets of concept symbols and role symbols. Concepts in π’œβ„’π’ž are of the following forms: βŠ₯ | 𝐴 | ¬𝐢 | 𝐢 βŠ“ 𝐷 | βˆƒπ‘Ÿ.𝐢 where 𝐴 ∈ 𝑁𝑐 , π‘Ÿ ∈ π‘π‘Ÿ and 𝐢 and 𝐷 are π’œβ„’π’ž concepts. We also allow the following abbreviations: ⊀ ≑ Β¬βŠ₯, βˆ€π‘Ÿ.𝐢 ≑ Β¬βˆƒπ‘Ÿ.¬𝐢, 𝐢 βŠ” 𝐷 ≑ Β¬(¬𝐢 βŠ“ ¬𝐷). An interpretation in π’œβ„’π’ž is a pair ℐ = βŸ¨Ξ”β„ , ·ℐ ⟩ where the domain Δℐ is a nonempty set and ·ℐ is an interpretation function that assigns to each concept symbol 𝐴 ∈ 𝑁𝑐 a subset of Δℐ and to each π‘Ÿ ∈ π‘π‘Ÿ a subset of Δℐ Γ— Δℐ . The language constructs are interpreted as follows: βŠ₯ℐ := βˆ…, (¬𝐢)ℐ := Δℐ βˆ–πΆ ℐ , (𝐢 βŠ“ 𝐷)ℐ := 𝐢 ℐ ∩ 𝐷ℐ , (βˆƒπ‘Ÿ.𝐢)ℐ := {π‘₯ ∈ Δℐ |βˆƒπ‘¦ : (π‘₯, 𝑦) ∈ π‘Ÿβ„ ∧ 𝑦 ∈ 𝐢 ℐ }. A TBox, or an ontology, is a set of axioms of the form 𝐢 βŠ‘ 𝐷, where 𝐢 and 𝐷 are concepts. ℐ is model of an ontology π’ͺ if all axioms 𝐢 βŠ‘ 𝐷 ∈ π’ͺ are true in ℐ, in symbols ℐ |= 𝐢 βŠ‘ 𝐷. And, ℐ |= 𝐢 βŠ‘ 𝐷 if and only if 𝐢 ℐ βŠ† 𝐷ℐ . We say that 𝐢 βŠ‘ 𝐷 is satisfiable with respect to π’ͺ if and only if ℐ |= 𝐢 βŠ‘ 𝐷 for some model ℐ of π’ͺ. We also say that 𝐢 βŠ‘ 𝐷 is a consequence of π’ͺ, in symbols π’ͺ |= 𝐢 βŠ‘ 𝐷, if and only if ℐ |= 𝐢 βŠ‘ 𝐷 for every model ℐ of π’ͺ. Let 𝐢 be an π’œβ„’π’ž concept, we denote ⋃︀ by 𝑠𝑖𝑔(𝐢) the set of concept and role symbols appearing in 𝐢. For an ontology π’ͺ, 𝑠𝑖𝑔(π’ͺ) = πΆβŠ‘π·βˆˆπ’ͺ 𝑠𝑖𝑔(𝐢) βˆͺ 𝑠𝑖𝑔(𝐷). The size of an ontology is the number of axioms in it. Definition 1. Two models ℐ and π’₯ Ξ£-coincide iff Δℐ = Ξ”π’₯ and 𝑝ℐ = 𝑝π’₯ for every concept or role symbol 𝑝 ∈ Ξ£. Definition 2. Let π’ͺ1 and π’ͺ2 be two ontologies and Ξ£ a set of symbols where Ξ£ βŠ† 𝑁𝑐 βˆͺ π‘π‘Ÿ . We say π’ͺ1 and π’ͺ2 are semantically Ξ£-equivalent, in symbols π’ͺ1 ≑ℳ Ξ£ π’ͺ2 , iff for every model ℐ1 of π’ͺ1 there is a model ℐ2 of π’ͺ2 , and vice versa, such that ℐ1 and ℐ2 Ξ£-coincide. Resolution (Res) 𝐢1 βŠ” 𝐴 𝐢2 βŠ” ¬𝐴 𝐢1 βŠ” 𝐢2 where 𝐴 is a forgetting symbol and 𝐢1 , 𝐢2 are general concept expressions. Figure 1: Binary resolution rule Definition 3. Let π’ͺ1 and π’ͺ2 be two π’œβ„’π’ž ontologies, and let Ξ£ a set of symbols where Ξ£ βŠ† 𝑁𝑐 βˆͺπ‘π‘Ÿ . We say π’ͺ1 and π’ͺ2 are deductively Ξ£-equivalent, in symbols π’ͺ1 ≑𝐢 Ξ£ π’ͺ2 , iff for every π’œβ„’π’ž concept inclusion 𝛼, where 𝑠𝑖𝑔(𝛼) βŠ† Ξ£, we have π’ͺ1 |= 𝛼 iff π’ͺ2 |= 𝛼. Deductive forgetting is defined using deductive equivalence [10]. Definition 4. Let π’ͺ be an π’œβ„’π’ž ontology, and let β„± βŠ† 𝑠𝑖𝑔(π’ͺ) ∩ 𝑁𝑐 be a forgetting signa- ture. An ontology 𝒱 is a deductive forgetting view of π’ͺ w.r.t. β„± iff 𝑠𝑖𝑔(𝒱) βŠ† 𝑠𝑖𝑔(π’ͺ)βˆ–β„±, and π’ͺ ≑𝐢 𝑠𝑖𝑔(π’ͺ)βˆ–β„± 𝒱. 4. Computing the Intermediate Ontology The first stage of our method is to compute the intermediate ontology π’ͺ𝑖𝑛𝑑 of the input on- tology π’ͺ w.r.t. the given forgetting signature β„±. The method applies resolution to the input ontology written in clausal form. π’ͺπ‘π‘™π‘Žπ‘’π‘ π‘Žπ‘™ is computed by: (1) converting π’ͺ into negation normal form (NNF), with negation applied only to concept names, (2) miniscoping, i.e., re- placing βˆƒπ‘Ÿ.𝐢 βŠ” βˆƒπ‘Ÿ.𝐷 with the semantically equivalent βˆƒπ‘Ÿ.(𝐢 βŠ” 𝐷), and βˆ€π‘Ÿ.𝐢 βŠ“ βˆ€π‘Ÿ.𝐷 with the semantically equivalent βˆ€π‘Ÿ.(𝐢 βŠ“ 𝐷), (3) applying structural transformations to extract the formulas under role restriction that contain the forgetting symbols by introducing fresh concept symbols (called definers) [28], and (4) converting the result to conjunctive normal form (CNF). Example 1. Consider the axiom 𝐴 βŠ‘ βˆƒπ‘Ÿ.(𝐡 βŠ“ 𝐢) where 𝐡 is a forgetting symbol. It is first converted to NNF by eliminating the connective βŠ‘, giving 𝑆1 = {¬𝐴 βŠ” βˆƒπ‘Ÿ.(𝐡 βŠ“ 𝐢)}. Structural transformation is applied to extract 𝐡 βŠ“ 𝐢, giving 𝑆2 = {¬𝐴 βŠ” βˆƒπ‘Ÿ.𝐷1 , ¬𝐷1 βŠ” (𝐡 βŠ“ 𝐢)} where 𝐷1 ∈ 𝑁𝑑 is a definer symbol. Finally, 𝑆2 is converted to CNF, giving 𝑆3 = {¬𝐴 βŠ” βˆƒπ‘Ÿ.𝐷1 , ¬𝐷1 βŠ” 𝐡, ¬𝐷1 βŠ” 𝐢}. The forgetting symbols in β„± are then eliminated from π’ͺπ‘π‘™π‘Žπ‘’π‘ π‘Žπ‘™ by iteratively eliminating them using the Resolution rule in Figure 1. When all possible resolution inferences have been performed on a concept symbol in β„±, clauses that contain this concept symbol are removed in a purity deletion step. Additionally, the following operations are applied eagerly: (1) Tautology deletion: clauses of the form 𝐢 βŠ” ¬𝐢 βŠ” 𝐸 are deleted, where 𝐢 and 𝐸 are π’œβ„’π’ž concepts. (2) Purification: if a forgetting symbol 𝐴 occurs only positively or only negatively in π’ͺ, then 𝐴 is replaced everywhere by ⊀ and βŠ₯ respectively. Assume π’ͺ𝑖𝑛𝑑 is the set of clauses that remain. Example 2. Let π’ͺ = {𝐴 βŠ‘ βˆ€π‘Ÿ.𝐡 βŠ“ βˆ€π‘ .¬𝐡, 𝐺 βŠ‘ βˆƒπ‘Ÿ.(¬𝐡 βŠ” 𝐢), 𝐡 βŠ‘ 𝐻}, and β„± = {𝐡}. The method starts by generating π’ͺπ‘π‘™π‘Žπ‘’π‘ π‘Žπ‘™ = {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐴 βŠ” βˆ€π‘ .𝐷2 , ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐷3 , ¬𝐷1 βŠ” 𝐡, ¬𝐷2 βŠ” ¬𝐡, ¬𝐷3 βŠ” ¬𝐡 βŠ” 𝐢, ¬𝐡 βŠ” 𝐻}, where 𝐷1 , 𝐷2 , and 𝐷3 are fresh definers. Then, it resolves on the concept symbol 𝐡 using the Resolution rule in Figure 1 generating additionally the clauses {¬𝐷1 βŠ” ¬𝐷2 , ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢, ¬𝐷1 βŠ” 𝐻}. Finally, the clauses {¬𝐷1 βŠ” 𝐡, ¬𝐷2 βŠ” ¬𝐡, ¬𝐷3 βŠ” ¬𝐡 βŠ” 𝐢, ¬𝐡 βŠ” 𝐻} are removed by purity deletion. So the intermediate ontology π’ͺ𝑖𝑛𝑑 is {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐴 βŠ” βˆ€π‘ .𝐷2 , ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐷3 , ¬𝐷1 βŠ” ¬𝐷2 , ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢, ¬𝐷1 βŠ” 𝐻}. Theorem 1. π’ͺ ≑ℳ 𝑖𝑛𝑑 𝑠𝑖𝑔(π’ͺ)βˆ–β„± π’ͺ . Theorem 2. The size of π’ͺ𝑖𝑛𝑑 is in the worst case exponential in the size of the given ontology π’ͺ and double exponential in the number of forgetting symbols. Definers are used in the intermediate ontology π’ͺ𝑖𝑛𝑑 to represent subsets of role successors. Precise definitions of definers cannot always be given without knowledge of the forgetting symbols. For instance in Example 1, 𝐷1 is interpreted as 𝐷1ℐ = {𝑦 ∈ 𝐡 ℐ ∩ 𝐢 ℐ | (π‘₯, 𝑦) ∈ π‘Ÿβ„ , π‘₯ ∈ 𝐴ℐ } where ℐ is a model of 𝑆. Since the user of the forgetting view may not be aware of 𝐡, a definition of 𝐷1 in terms of 𝐡 is not conveyed in π’ͺ𝑖𝑛𝑑 . Thus, definers may be viewed as second-order existentially quantified concept symbols because they represent some subsets of the domain whose definitions cannot be precisely captured. One can observe that π’ͺ𝑖𝑛𝑑 can be viewed as an approximation to the semantic forgetting view of π’ͺ with respect to β„±. 5. Extracting Ξ” and π’ͺπ‘Ÿπ‘’π‘‘ The second stage of the method is to obtain the sets Ξ” and π’ͺπ‘Ÿπ‘’π‘‘ from π’ͺ𝑖𝑛𝑑 , where π’ͺπ‘Ÿπ‘’π‘‘ is an ontology approximating the deductive view and Ξ” is the information difference between π’ͺ𝑖𝑛𝑑 and π’ͺπ‘Ÿπ‘’π‘‘ . The Reduction rule in Figure 2 removes from π’ͺ𝑖𝑛𝑑 the clauses with two or more negative definers. These clauses constitute the set Ξ”. The Role Propagation rule in Figure 2 computes the π’œβ„’π’ž consequences that are otherwise lost when removing the clauses of Ξ” from π’ͺ𝑖𝑛𝑑 by the Reduction rule. Therefore, we require it to be applied before removing these clauses. The premises of the Role Propagation rule start with the clause 𝑃0 βŠ” 𝐢0 , where 𝑃0 takes the form ¬𝐷0 βŠ” ¬𝐷1 βŠ” Β· Β· Β· βŠ” ¬𝐷𝑛 . The second premise is a set of clauses 𝑃𝑗 βŠ” 𝐢𝑗 . Here, the concepts 𝑃𝑗 takes the same form as the concept 𝑃0 , i.e., is a disjunction of negative definers, but also Definers(𝑃𝑗 ) βŠ† Definers(𝑃0 ) where Definers(𝑃 ) denotes the set of definer symbols in 𝑠𝑖𝑔(𝑃 ). The intuition here is that 𝑃𝑗 βŠ‘ 𝑃0 . Therefore, every domain element that is not in the interpretation of 𝑃0 , consequently 𝑃𝑗 , must be in the interpretation of 𝐢0 and 𝐢𝑗 . The clauses in the third and the fourth premises take the same form, except that existential role restriction is only allowed in the third premise. ⨆︀𝑛 By the thirddand fourth premises, every domain element must be in the interpretation of d 𝑖=0 𝐸𝑖 or π’¬π‘Ÿ.( 𝑛𝑖=0 𝐷𝑖 ). But the latter can be rewritten as π’¬π‘Ÿ.¬𝑃0 , which is subsumed by π’¬π‘Ÿ.( π‘š 𝑗=0 𝐢𝑗 ) as concluded by the rule. Example 3. Continuing with Example 2, the Role Propagation rule applies with its four premises being: 1. 𝑃0 βŠ” 𝐢0 = ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢 Role Propagation π‘š ⋃︀ 𝑛 ⋃︀ 𝑃0 βŠ” 𝐢0 , {𝑃𝑗 βŠ” 𝐢𝑗 },𝐸0 βŠ” π’¬π‘Ÿ.𝐷0 , {𝐸𝑖 βŠ” βˆ€π‘Ÿ.𝐷𝑖 } 𝑗=1 𝑖=1 𝑛 ⨆︀ π‘š d ( 𝐸𝑖 ) βŠ” π’¬π‘Ÿ.( 𝐢𝑗 ) 𝑖=0 𝑗=0 𝑛 ⨆︀ where 𝑃0 = ¬𝐷𝑖 , 𝑃𝑗 is any sub-concept of 𝑃0 , 𝒬 ∈ {βˆƒ, βˆ€}, and 𝐢0 and 𝐢𝑗 do not contain a 𝑖=0 definer. Reduction π’ͺ βˆͺ {¬𝐷1 βŠ” ... βŠ” ¬𝐷𝑛 βŠ” 𝐢} π’ͺ where 𝐢 is a concept expression that does not contain a negative definer, 𝐷1 , ..., 𝐷𝑛 are definer symbols, and 𝑛 β‰₯ 2. Figure 2: π’œβ„’π’ž reduction rules. π‘š ⋃︀ 2. {𝑃𝑗 βŠ” 𝐢𝑗 } = {¬𝐷1 βŠ” 𝐻} 𝑗=1 3. 𝐸0 βŠ” π’¬π‘Ÿ.𝐷 = ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐷3 𝑛 ⋃︀ 4. {𝐸𝑖 βŠ” βˆ€π‘Ÿ.𝐷𝑖 } = {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 } 𝑖=1 The conclusion is ¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.(𝐢 βŠ“ 𝐻). Note that the generated conclusion preserves information that would otherwise be lost when the clause ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢 is removed by the Reduction rule. After the Role Propagation rule has been exhaustively applied, the clauses of Ξ” are removed. The remaining clauses constitute π’ͺπ‘Ÿπ‘’π‘‘ . Denote by π’ͺπ‘Ÿπ‘ the ontology obtained from π’ͺ𝑖𝑛𝑑 by applying the Role Propagation rule. Example 4. Continuing with Example 2. We have π’ͺπ‘Ÿπ‘ = π’ͺ𝑖𝑛𝑑 βˆͺ {¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.(𝐢 βŠ“ 𝐻)} where the axiom on the right of the union operator is the conclusion of the Role Propagation rule obtained in Example 3. We also have Ξ” = {¬𝐷1 βŠ” ¬𝐷2 , ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢}, and π’ͺπ‘Ÿπ‘’π‘‘ = {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐴 βŠ” βˆ€π‘ .𝐷2 , ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐷3 , ¬𝐷1 βŠ” 𝐻, ¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.(𝐢 βŠ“ 𝐻)}. Theorem 3. π’ͺπ‘Ÿπ‘ ≑𝐢 𝑠𝑖𝑔(π’ͺ)βˆ–β„± π’ͺ π‘Ÿπ‘’π‘‘ . Theorem 3 proves a main contribution of the paper. First, observe that π’ͺπ‘Ÿπ‘ ≑ℳ 𝑖𝑛𝑑 𝑠𝑖𝑔(π’ͺ)βˆ–β„± π’ͺ . It follows from this observation, and Theorems 1 and 3 that π’ͺ ≑𝐢 𝑠𝑖𝑔(π’ͺ)βˆ–β„± π’ͺ π‘Ÿπ‘’π‘‘ . Therefore, if π’ͺ𝑒𝑖 is a deductive view of π’ͺπ‘Ÿπ‘’π‘‘ with respect to 𝑠𝑖𝑔(π’ͺ)βˆ–β„±, then π’ͺπ‘Ÿπ‘’π‘‘ is deductively equivalent to π’ͺ𝑒𝑖 with respect to 𝑠𝑖𝑔(π’ͺ)βˆ–β„±. We shall strengthen this in the next section and show that if no cycles occur in π’ͺπ‘Ÿπ‘’π‘‘ then it is semantically equivalent to the deductive view with respect to 𝑠𝑖𝑔(π’ͺ)βˆ–β„±. Second, observe that π’ͺπ‘Ÿπ‘ = π’ͺπ‘Ÿπ‘’π‘‘ βˆͺ Ξ”. Additionally, the clauses in Ξ” have been generated in π’ͺ𝑖𝑛𝑑 by resolution inferences over the forgetting symbols, and the premises of these inferences were removed by purity deletion. Therefore, we find in general that π’ͺπ‘Ÿπ‘’π‘‘ ΜΈ|= Ξ”. This implies that Ξ” can be viewed as representing the information difference between π’ͺπ‘Ÿπ‘ and π’ͺπ‘Ÿπ‘’π‘‘ . Altogether we therefore conclude that Ξ” can be viewed as the information difference between π’ͺ and the deductive view with respect to 𝑠𝑖𝑔(π’ͺ)βˆ–β„±. We end this section with a discussion on the extracted set Ξ” which consists of clauses of the format ¬𝐷1 βŠ” Β· Β· Β· βŠ” ¬𝐷𝑛 βŠ” 𝐹 where 𝑛 β‰₯ 2, or in axiom form, 𝐷1 βŠ“ Β· Β· Β· βŠ“ 𝐷𝑛 βŠ‘ 𝐹 . Since we introduced the definer symbols to represent subsets of role successors, these clauses can be understood as information on the conjunctions of different subsets of role successors. For instance, in Example 2, the clause ¬𝐷1 βŠ” ¬𝐷2 ∈ Ξ” specifies the constraint that the subset of π‘Ÿ-successors and the subset of 𝑠-successors of domain elements in the interpretation of 𝐴 are disjoint. It was not a coincidence that we introduced definer symbols to represent subsets of role successors. Using them in this way and introducing them via structural transformation forces the clauses in Ξ” to be explicit members of π’ͺ𝑖𝑛𝑑 which simplifies their extraction, giving us a representation of the difference between π’ͺ and the deductive view. 6. Eliminating the Definer Symbols We identified Ξ” as the axioms that contain two or more negative definers. π’ͺ𝑖𝑛𝑑 and π’ͺπ‘Ÿπ‘’π‘‘ may contain definer symbols that appear negatively in clauses where no other negative definer is present. These definers can be eliminated safely while preserving the interpretations of the non-forgotten vocabulary. For this, we use the Definer Elimination rule in Figure 3. The side conditions of the Definer Elimination rule exclude the elimination of definers that may appear both positively and negatively in a clause. We call such definer symbols cyclic definers. The existence of cyclic definers signifies cycles in the original ontology over some forgetting symbols. In this case the deductive view may not exist as it requires an infinite representation. An approach to eliminate cyclic definers and obtain a finite approximation of the deductive view is using fixpoint operators [12]. As an alternative, cyclic definers can be left in the deductive view as witnesses of these cycles [13]. We find this the best option because it defers the decision of a suitable representation to a later stage. For clauses that contain only one negative definer symbol, possibly with other positive definers, the Definer Elimination rule in Figure 3 is applied exhaustively. The rule replaces the definer symbol 𝐷 with its super-concept 𝐢1 βŠ“ ... βŠ“ 𝐢𝑛 . Note that, in the Definer Elimination rule, 𝐢 may be βŠ₯. Besides the Definer Elimination rule, we also eagerly apply the Tautology Deletion and the Purification rules (see Section 4). Example 5. Continuing with Example 4, 𝒱 is extracted from π’ͺπ‘Ÿπ‘’π‘‘ as follows: 1. The definers 𝐷2 and 𝐷3 are eliminated using Purification. Since 𝐷2 and 𝐷3 appear only pos- itively in π’ͺπ‘Ÿπ‘’π‘‘ , they are purified by replacing them with ⊀ which gives {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐴 βŠ” βˆ€π‘ .⊀, ¬𝐺 βŠ” βˆƒπ‘Ÿ.⊀, ¬𝐷1 βŠ” 𝐻, ¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.(𝐢 βŠ“ 𝐻)}. As βˆ€π‘ .⊀ evaluates to ⊀, the result can be simplified further to {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐺 βŠ” βˆƒπ‘Ÿ.⊀, ¬𝐷1 βŠ” 𝐻, ¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.(𝐢 βŠ“ 𝐻)}. Definer Elimination π’ͺ βˆͺ {¬𝐷 βŠ” 𝐢1 , ..., ¬𝐷 βŠ” 𝐢𝑛 } π’ͺ[𝐷/𝐢] where 𝐢 = βŠ“π‘›π‘–=1 𝐢𝑖 and 𝐷 ∈ / 𝑠𝑖𝑔(𝐢), 𝐢 does not contain any negative definers, and π’ͺ does not contain 𝐷 negatively. Figure 3: Definer elimination rule 2. The definer 𝐷1 is eliminated by the Definer Elimination rule in Figure 3 giving {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐻, Β¬πΊβŠ”βˆƒπ‘Ÿ.⊀, ¬𝐻 βŠ”π», Β¬π΄βŠ”Β¬πΊβŠ”βˆƒπ‘Ÿ.(𝐢 βŠ“π»)}. The clause ¬𝐻 βŠ”π» is then eliminated by Tautology Deletion giving 𝒱 = {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐻, ¬𝐺 βŠ” βˆƒπ‘Ÿ.⊀¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.(𝐢 βŠ“ 𝐻)} Theorem 4. Let 𝒱 be generated from π’ͺπ‘Ÿπ‘’π‘‘ by applying the Definer Elimination rule from Figure 3 exhaustively. Then, (1) π’ͺπ‘Ÿπ‘’π‘‘ ≑ℳ𝑠𝑖𝑔(π’ͺ)βˆ–β„± 𝒱; and (2) if 𝑠𝑖𝑔(𝒱) ∩ 𝑁𝑑 = βˆ… then 𝒱 is a deductive forgetting view of π’ͺ w.r.t. β„±. 7. Computing More Informative Forgetting Views Our forgetting method allows customizing the informativeness of the final forgetting view according to user requirements, which reveals a spectrum of forgetting views that are more informative than the deductive view and at most as informative as the intermediate ontology. This can be done by overriding the Reduction rule as illustrated in the following example. Example 6. Consider π’ͺ𝑖𝑛𝑑 from Example 2. Applying the rules in Figure 2 gives π’ͺπ‘Ÿπ‘’π‘‘ and Ξ” from Example 4. We may increase the informativeness of the final forgetting view by overriding the Reduction rule. We describe three different forgetting views that can be generated in this way. 1. If we want to preserve all the information about the π‘Ÿ-successors of 𝐴, then we override the Reduction rule to retain the clauses where 𝐷1 occurs. In this case, Ξ”1 = βˆ… and the final forgetting view will be π’ͺ1π‘Ÿπ‘’π‘‘ = 𝒱1 = {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐴 βŠ” βˆ€π‘ .𝐷2 , ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐷3 , ¬𝐷1 βŠ” ¬𝐷2 , ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢, ¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐢}. 2. If we want to preserve the information about the π‘Ÿ-successors of 𝐴 in relation to the π‘Ÿ- successors of 𝐺, we override the Reduction rule to retain the clauses where both 𝐷1 and 𝐷3 occur. That is, Ξ”2 = {¬𝐷1 βŠ” ¬𝐷2 } and ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢 ̸∈ Ξ”. Then, π’ͺ2π‘Ÿπ‘’π‘‘ = {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐴 βŠ” βˆ€π‘ .𝐷2 , ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐷3 , ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢, ¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐢}, and 𝒱2 = {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐷3 , ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢, ¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐢} with 𝐷2 purified away. 3. If we are interested in the relation between the π‘Ÿ and 𝑠 successors of 𝐴, then we override the Reduction rule to remove ¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢 but not ¬𝐷1 βŠ” ¬𝐷2 . That is Ξ”3 = {¬𝐷1 βŠ” ¬𝐷3 βŠ” 𝐢}. Consequently, we get π’ͺ3π‘Ÿπ‘’π‘‘ = {¬𝐴 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐴 βŠ” βˆ€π‘ .𝐷2 , ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐷3 , ¬𝐴 βŠ” Β¬πΊβŠ”βˆƒπ‘Ÿ.𝐢, ¬𝐷1 βŠ”Β¬π·2 }. The final forgetting view then becomes 𝒱3 = {Β¬π΄βŠ”βˆ€π‘Ÿ.𝐷1 , Β¬π΄βŠ” βˆ€π‘ .𝐷2 , ¬𝐺 βŠ” βˆƒπ‘Ÿ.⊀, ¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐢, ¬𝐷1 βŠ” ¬𝐷2 } with 𝐷3 purified away. Observe that in 𝒱1 and 𝒱2 the clause ¬𝐴 βŠ” ¬𝐺 βŠ” βˆƒπ‘Ÿ.𝐢 is redundant. We can eliminate this redundancy by applying the Role Propagation rule only when a premise of the rule occurs in Ξ”. Since the final forgetting views may use definers, the following question may be asked: Are definers in forgetting views limiting? We argue that since definers are existentially quantified and the forgetting view is expressed using π’œβ„’π’ž syntax, standard reasoning tasks such as satisfiability checking, and query answering, can be performed with respect to the non-forgotten vocabulary using the existing π’œβ„’π’ž methods. The following example explains the idea. Example 7. Let ontology π’ͺ = {𝐴1 βŠ‘ βˆ€π‘Ÿ.𝐡, 𝐴2 βŠ‘ βˆ€π‘Ÿ.¬𝐡} be an ontology, and π’ͺ𝑖𝑛𝑑 = {¬𝐴1 βŠ” βˆ€π‘Ÿ.𝐷1 , ¬𝐴2 βŠ” βˆ€π‘Ÿ.𝐷2 , ¬𝐷1 βŠ” ¬𝐷2 βŠ‘ βŠ₯} the intermediate ontology of π’ͺ with respect to β„± = {𝐡} where 𝐷1 and 𝐷2 are definers. Assume Ξ” = βˆ…, then π’ͺ𝑖𝑛𝑑 is the final forgetting view. Both π’ͺ and π’ͺ𝑖𝑛𝑑 model the information that the π‘Ÿ-successors of the elements in the interpretation of 𝐴1 are disjoint from the π‘Ÿ-successors of the elements in the interpretation of 𝐴2 . Suppose we additionally have a database π’œ = {𝐴1 (π‘Ž1 ), 𝐴2 (π‘Ž2 ), π‘Ÿ(π‘Ž1 , 𝑏)}, and we want to prove the unsatisfiability of π‘Ÿ(π‘Ž2 , 𝑏) with respect to the knowledge base consisting of π’ͺ and π’œ. This can be done by using a standard π’œβ„’π’ž reasoner to show that π’ͺ, π’œ, π‘Ÿ(π‘Ž2 , 𝑏) |= βŠ₯. Replacing π’ͺ with π’ͺ𝑖𝑛𝑑 , would still prove the unsatisfiability of π‘Ÿ(π‘Ž2 , 𝑏). Moreover, the reasoner does not require the full interpretation of 𝐷1 and 𝐷2 to prove that π’ͺ𝑖𝑛𝑑 , π’œ, π‘Ÿ(π‘Ž2 , 𝑏) |= βŠ₯. 8. Evaluation We implemented a prototype of our method based on Java 12 and the OWL API 5.1.11. We refer to our prototype as SeD. We used a random corpus of 50 ontologies from the NCBO Bioportal repository to perform the evaluation. Details of the corpus are given in the long version. We performed two evaluations, each corresponding to a different selection of the forgetting signature β„±. Evaluation 1 selected β„± as a segment of the 𝑁𝑐 sorted by name (recall that 𝑁𝑐 is the set of concept names of the input ontology), so β„± contained related concept names. E.g., β€˜Abdomen’ and β€˜Abdomen-pain’ were likely to be together in β„± as they would be adjacent in the sorted 𝑁𝑐 . The intuition was to simulate the use case of extracting the knowledge of a single topic, e.g., the digestive system from a large biomedical ontology. Evaluation 2 selected the concept names that occurred most frequently under role restrictions, aiming for more definers being introduced in π’ͺ𝑖𝑛𝑑 and bigger Ξ” sets. The intuition was to simulate the worst case when the information difference between the intermediate ontology and the deductive views would be large, and the performance of our two-stage forgetting method would be expected to degrade. In every evaluation and for each ontology in the corpus, three forgetting experiments were performed to forget 10%, 30%, and 50% of concept symbols in 𝑁𝑐 giving a total of 150 experiments in each evaluation. Each experiment compared SeD and Lethe (version 2.11-0.026)1 [15]. Lethe is an implementation of the deductive forgetting method in [13]. Each tool was allocated 2GB of memory and five hours time out. All experiments were run on a x64-based processor Intel(R) Core(TM) i5 CPU @ 2.7GHz with a 64-bit operating system (macOS Catalina 10.15.7). 1 http://www.cs.man.ac.uk/~koopmanp/lethe/index.html Table 1 Timeouts of SeD and Lethe Evaluation 1 Evaluation 2 10% 30% 50% 10% 30% 50% SeD 2 3 5 2 3 3 Lethe 2 7 8 1 6 7 Figure 4: Normal Distribution of the Gain values. Range of X-axes is Average Β± 3 Standard Deviations Table 1 shows the timeouts of SeD and Lethe. SeD appeared to be more reliable than Lethe in both evaluations. Also, SeD was less affected by increasing the size of β„± from 10% to 30% to 50% of 𝑁𝑐 , suggesting that SeD is more scalable to harder problems than Lethe. Next we compared the execution times of SeD and Lethe to compute the deductive view. We first computed the time gained by using SeD over Lethe with the formula Gain = (𝑇𝐿 βˆ’ 𝑇𝑆 )/𝑇𝐿 , where 𝑇𝐿 and 𝑇𝑆 are the times consumed by Lethe and SeD respectively. Second, we computed the averages and standard deviations of the Gain values. In line with standard data analysis methods, outliers were excluded. These were experiments with extreme Gain values compared to the rest of the experiments. In Evaluation 1 we excluded two experiments in the 10% setting and one in the 50% setting, whereas in Evaluation 2 we excluded one experiment in the 10% setting and one from the 50% setting. The averages and standard deviations in Evaluation 1 were: (0.58, 0.78), (0.60, 0.68), and (0.66, 0.68) in the 10%, 30%, and 50% settings respectively. In Evaluation 2 they were: (0.65, 0.46), (0.74, 0.50), and (0.74, 0.67) in the 10%, 30%, and 50% settings respectively. Figure 4 shows the normal distributions of the Gain values in the three settings in the two evaluations. The graphs reflect the attained positive averages stated above, and compare the gain values across the three settings in each evaluation, also allowing the two evaluations to be compared. Surprisingly, a better and more consistent performance was found in Evaluation 2 over Evaluation 1, against our expectation that Evaluation 2 would represent the worst case scenario for SeD. This is indicated by the higher peaks indicating higher probability of achieving the average Gain, and the narrower curves indicating less variation in the results. The performance improvement happens due to the forgetting method itself not the corpus. While Lethe translates the input ontology to a clausal form that is similar to ours, it disallows clauses with two or more negative definers. To compensate for this restriction, Lethe introduces definer symbols as part of the forgetting calculus, and builds a subsumption hierarchy between the definers. This hierarchy forces extra resolution inferences to be performed. The following example illustrates dynamic introduction of definers in Lethe. Example 8. Let π’ͺ = {𝐴1 βŠ‘ βˆƒπ‘Ÿ.¬𝐡, 𝐴2 βŠ‘ βˆ€π‘Ÿ.𝐡}, and β„± = {𝐡}. Lethe generates π’ͺπ‘π‘™π‘Žπ‘’π‘ π‘Žπ‘™ as {¬𝐴1 βŠ” βˆƒπ‘Ÿ.𝐷1 , ¬𝐴2 βŠ” βˆ€π‘Ÿ.𝐷2 , ¬𝐷1 βŠ” ¬𝐡, ¬𝐷2 βŠ” 𝐡}. Instead of resolving 𝐡 directly to compute the clause ¬𝐷1 βŠ” ¬𝐷2 , Lethe introduces a new definer 𝐷3 and generates an intermediate ontology π’ͺ1 = π’ͺπ‘π‘™π‘Žπ‘’π‘ π‘Žπ‘™ βˆͺ {¬𝐴1 βŠ” ¬𝐴2 βŠ” βˆƒπ‘Ÿ.𝐷3 , ¬𝐷3 βŠ” 𝐷1 , ¬𝐷3 βŠ” 𝐷2 }. The last two clauses on π’ͺ1 are resolved with ¬𝐷1 βŠ” ¬𝐡 and ¬𝐷2 βŠ” 𝐡 to give ¬𝐷3 βŠ” ¬𝐡 and ¬𝐷3 βŠ” 𝐡 which in turn are resolved together to give ¬𝐷3 . All clauses where 𝐡 occurs are then removed to give π’ͺ2 = {¬𝐴1 βŠ” βˆƒπ‘Ÿ.𝐷1 , ¬𝐴2 βŠ” βˆ€π‘Ÿ.𝐷2 , ¬𝐴1 βŠ” ¬𝐴2 βŠ” βˆƒπ‘Ÿ.𝐷3 , ¬𝐷3 }. The definers 𝐷1 , 𝐷2 , and 𝐷3 are eliminated in a similar way to the method described in Section 6 giving 𝒱 = {¬𝐴1 βŠ” βˆƒπ‘Ÿ.⊀, ¬𝐴1 βŠ” ¬𝐴2 }. Our normal form is more flexible as it allows several negative definers to appear in a clause, thus avoids the extra resolution inferences performed by Lethe. We measured the size of the extracted Ξ” set. In Evaluation 1, Ξ” was on average 0.01%, 0.66%, and 18.3% of the size of the original ontology, in the 10%, 30%, and 50% settings respectively. In Evaluation 2, Ξ” was on average 0.23%, 0.88%, and 7.13% of the size of the original ontology, in the 10%, 30%, and 50% settings respectively. We also measured the number of definers in Ξ” as a ratio to the forgetting signature. In Evaluation 1, they were on average 0.03%, 0.63%, and 1.5% in the 10%, 30%, and 50% settings respectively. In Evaluation 2, they were on average 0.04%, 0%, and 1.4% in the 10%, 30%, and 50% settings respectively. These ratios indicate that our fine-grained method was feasible since appending π’ͺπ‘Ÿπ‘’π‘‘ with axioms from Ξ” introduced few definers relative to the size of β„±. Finally, we measured the size of the deductive view relative to the original ontology. In Evaluation 1 it was on average 114%, 103%, and 117% of the size of the original ontology in the 10%, 30%, and 50% settings respectively. In Evaluation 2, it was on average 113%, 95%, and 103% of the size of the original ontology in the 10%, 30%, and 50% settings respectively. 9. Conclusions and Future Work We presented a new forgetting method that performs deductive forgetting, and extracts a set Ξ” of axioms representing the information difference between the original ontology and the deductive view. Not only does this give a clearer understanding, in terms of the modelled information, on the difference between the input ontology and the deductive view, but also it allows a fine-grained forgetting system that gives control over the information modelled in the forgetting view. Empirical evaluation suggests that our forgetting method is faster than the state-of-the-art forgetting tool Lethe despite computing more information. Nevertheless, our evaluation suggested that appending the deductive forgetting view with information from Ξ” introduces few foreign symbols compared to the forgotten symbols. The final forgetting view therefore remains a compact extract of the original ontology for the use in applications. Future work will study in greater depth the newly revealed spectrum of forgetting variants, and their intersections with other forgetting variants in the literature. References [1] M. Ludwig, B. Konev, Practical uniform interpolation and forgetting for π’œβ„’π’ž TBoxes with applications to logical difference, in: Proc. KR 2014, AAAI Press, 2014. [2] B. C. Grau, B. Motik, Pushing the limits of reasoning over ontologies with hidden content, in: Proc. KR 2010, AAAI Press, 2010, pp. 214–224. URL: http://www.comlab.ox.ac.uk/ people/Boris.Motik/pubs/gm10pushing-ibq.pdf. [3] W. Del-Pinto, R. A. Schmidt, ABox abduction via forgetting in ALC, in: Proc. AAAI 2019, AAAI Press, 2019, pp. 2768–2775. [4] J. Lang, P. Marquis, Reasoning under inconsistency: A forgetting-based approach, Artificial Intelligence 174 (2010) 799–823. URL: https://www.sciencedirect.com/science/article/pii/ S0004370210000676. doi:https://doi.org/10.1016/j.artint.2010.04.023. [5] D. Subramanian, M. R. Genesereth, The relevance of irrelevance., in: Proc. IJCAI, 1987. [6] G. Lakemeyer, Relevance from an Epistemic Perspective, Artif. Intell. 97 (1997) 137–167. doi:10.1016/S0004-3702(97)00038-6. [7] J. Lang, P. Liberatore, P. Marquis, Propositional independence: Formula-variable indepen- dence and forgetting, Artificial Intelligence Research 18 (2003) 391–443. [8] E. Erdem, P. Ferraris, Forgetting Actions in Domain Descriptions, in: Proc. AAAI 2007, AAAI Press, 2007, pp. 409–414. [9] Y. Zhang, Y. Zhou, Knowledge forgetting: Properties and applications, Artificial Intelli- gence 173 (2009) 1525–1537. doi:10.1016/j.artint.2009.07.005. [10] C. Lutz, F. Wolter, Foundations for uniform interpolation and forgetting in expressive description logics, in: Proc. IJCAI 2011, 2011, p. 989–995. [11] J. Delgrande, A Knowledge Level Account of Forgetting, Artificial Intelligence Research 60 (2017) 1165–1213. doi:10.1613/jair.5530. [12] A. Nonnengart, A. Szalas, A fixpoint approach to second-order quantifier elimination with applications to correspondence theory, in: Logic at Work, Springer, 1998. [13] P. Koopmann, R. A. Schmidt, Uniform interpolation of π’œβ„’π’ž-ontologies using fixpoints, in: Proc. FroCoS 2013, volume 8152 of LNAI, Springer, 2013, pp. 87–102. [14] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, P. F. Patel-Schneider, The Description Logic Handbook, Cambridge Univ. Press, 2003. [15] P. Koopmann, R. A. Schmidt, Implementation and evaluation of forgetting in ALC- ontologies, in: Proc. WoMo 2013, volume 1081, CEUR-WS.org, 2013. [16] F. Lin, R. Reiter, Forget it, in: AAAI Fall Symp. on Relevance, 1994, pp. 154–159. [17] D. M. Gabbay, H. J. Ohlbach, Quantifier elimination in second-order predicate logic, in: Proc. KR 1992, Morgan Kaufmann, 1992, pp. 425–435. [18] Y. Zhang, Y. Zhou, Forgetting revisited, in: Proc. KR, AAAI Press, 2010. [19] S. Ghilardi, An algebraic theory of normal forms, Ann. Pure Appl. Logic 71 (1995) 189 – 245. [20] A. Herzig, J. Mengin, Uniform interpolation by resolution in modal logic, in: Proc. JELIA 2008, volume 5293 LNAI, Springer, 2008, pp. 219–231. [21] H. Ditmarsch, A. Herzig, J. Lang, P. Marquis, Introspective forgetting, in: Proc. AI 2008, Springer, 2008, pp. 18–29. [22] B. Konev, D. Walther, F. Wolter, Forgetting and uniform interpolation in large-scale description logic terminologies, in: Proc. IJCAI 2009, Morgan Kaufmann, 2009, p. 830–835. [23] B. Konev, C. Lutz, D. Walther, F. Wolter, Model-theoretic inseparability and modularity of description logic ontologies, Artificial Intelligence 203 (2013) 66–103. doi:10.1016/j. artint.2013.07.004. [24] E. Botoeva, B. Konev, C. Lutz, V. Ryzhikov, F. Wolter, M. Zakharyaschev, Inseparability and conservative extensions of description logic ontologies: A survey, in: Reasoning Web 2016, Springer, 2017, pp. 27–89. URL: https://doi.org/10.1007/978-3-319-49493-7_2. doi:10.1007/978-3-319-49493-7_2. [25] C. Lutz, F. Wolter, Deciding inseparability and conservative extensions in the description logic β„°β„’, Symbolic Computation 45 (2010) 194–228. doi:10.1016/j.jsc.2008.10.007. [26] G. D’Agostino, M. Hollenberg, Uniform interpolation, automata and the modal πœ‡-calculus, Logic Group Preprint Series 165 (1996). [27] D. Calvanese, G. De Giacomo, M. Lenzerini, Reasoning in Expressive Description Log- ics with Fixpoints Based on Automata on Infinite Trees, in: Proc. IJCAI 1999, Morgan Kaufmann, 1999, pp. 84–89. [28] A. Nonnengart, C. Weidenbach, Computing small clause normal forms, in: Handbook of Automated Reasoning, North-Holland, 2001, pp. 335 – 367.