Fine-Grained Forgetting for the Description Logic ALC

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 ofers solutions for many applications such as: computing logical diference [ 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 ifxpoint 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 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 nonforgotten 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 diference between the intermediate ontology and . If all foreign symbols are successfully eliminated from , then Δ also represents the information diference between the input ontology and the deductive view.

Several benefits are obtained from our forgetting method. (1) In two diferent 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 diference between the input ontology and the deductive view as information on the conjunctions of diferent 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 elimination [ 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 if Δℐ = Δ 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, if 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. 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, if for every ℒ concept inclusion , where ( ) ⊆ Σ, we have 1 |= if 2 |= .

Deductive forgetting is defined using deductive equivalence [ 10 ].

Definition 4. Let be an ℒ ontology, and let ℱ ⊆ () ∩ be a forgetting signature. An ontology is a deductive forgetting view of w.r.t. ℱ if ( ) ⊆ ()∖ℱ , and ≡ ()∖ℱ .

4. Computing the Intermediate Ontology

The first stage of our method is to compute the intermediate ontology of the input ontology 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., replacing ∃. ⊔ ∃. 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 diference 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 third and fourth premises, every domain element must be in the interpretation of ⨆︀ =0 or .(d=0 ). But the latter can be rewritten as .¬0, which is subsumed by .(d=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 definer.

Reduction

where 0 = ⨆︀ ¬, is any sub-concept of 0, ∈ {∃, ∀}, and 0 and do not contain a =0 ∪ {¬1 ⊔ ... ⊔ ¬ ⊔ }

where is a concept expression that does not contain a negative definer, 1, ..., are definer symbols, and ≥ 2. 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 diference between and . Altogether we therefore conclude that Δ can be viewed as the information diference 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 diferent 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 diference 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 positively 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. 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 diferent 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 = 1 = {¬ ⊔ ∀.1, ¬ ⊔ ∀.2, ¬ ⊔ ∃.3, ¬1 ⊔ forgetting view will be 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 ⊔ = {¬ ⊔ ∀.1, ¬ ⊔ ∀.2, ¬ ⊔ ∃.3, ¬ ⊔ ¬3 ⊔ }. Consequently, we get 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 diferent 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 diference 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).

1http://www.cs.man.ac.uk/~koopmanp/lethe/index.html

Table 1 shows the timeouts of SeD and Lethe. SeD appeared to be more reliable than Lethe in both evaluations. Also, SeD was less afected 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 ifrst 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 diference between the original ontology and the deductive view. Not only does this give a clearer understanding, in terms of the modelled information, on the diference 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. 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 Logics 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.

References

[1] M. Ludwig , B. Konev , Practical uniform interpolation and forgetting for ℒ TBoxes with applications to logical diference , 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 independence 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 Intelligence 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 ALContologies , 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