=Paper= {{Paper |id=Vol-3263/paper-17 |storemode=property |title=Fine-Grained Forgetting for the Description Logic ALC |pdfUrl=https://ceur-ws.org/Vol-3263/paper-17.pdf |volume=Vol-3263 |authors=Mostafa Sakr,Renate A. Schmidt |dblpUrl=https://dblp.org/rec/conf/dlog/SakrS22 }} ==Fine-Grained Forgetting for the Description Logic ALC== https://ceur-ws.org/Vol-3263/paper-17.pdf 
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.