In previous research, a number of practical approaches have been developed to perform forgetting. Generally, these tools fall within two categories: those which use resolution and others which use methods that exploit Ackermann's Lemma. The aim of this research was to compare the solutions being computed between the different methods using real world ontologies. The three tools used to represent the different approaches analyzed in this research are SCAN [2,5], LETHE [3,4], and FAME [6].
The first tool, SCAN, computes forgetting solutions for knowledge-bases expressed in first-order logic using a resolution-based approach, namely the SCAN algorithm [2]. Since forgetting in first-order logic is not generally solvable, SCAN is not guaranteed to find a solution. SCAN uses Skolemization to eliminate existential quantifiers, and therefore Skolem terms may appear in SCAN's solutions.
Similarly, LETHE, the second tool, computes its forgetting solution for description logic-based ontologies using a resolution-based method. However, it has been proven that the approach used to develop LETHE will find forgetting solutions for the description logics it can handle [3]. Furthermore, a point that will be useful later is that the forgetting solutions computed using LETHE may involve definer symbols, which are not part of the original vocabulary. This is due to applying flattening techniques to the ontology and sometimes failing to eliminate the extra symbols introduced during the computation [3].
Finally, the last tool, FAME, computes its forgetting solutions for description logic-based ontologies using a method based on Ackermann's Lemma. Similar to LETHE, the method is guaranteed to terminate. However, the method is not forgetting complete and may fail to eliminate some of the symbols [6]. The symbols it fails to eliminate are present in the result computed by the system.
The difference between the tools lie in the expressivity of the logics being supported, as well as the forgetting methodology being used. The aim of this research was to apply one of the forgetting tools, LETHE, to description logicbased ontologies to investigate the solutions computed, and compare them with those computed using SCAN and FAME. The focus was on concept forgetting in the description logic ALC.
For the purposes of the comparison in this research, a tool has been developed to investigate the solutions computed using LETHE, which were then compared with those computed using SCAN and FAME. FAME and LETHE have the advantage of being able to process large ontologies, hence two separate versions of the system were created: one that compares LETHE and SCAN, and another that compares FAME and LETHE using larger ontologies. An effort has been made to maximize the size of the ontologies that SCAN can accept. However, the considered ontologies were still not as large as desired. This is due to boundaries in the static data structures of SCAN. O expressed in description logic in the OWL syntax, using the OWL API, and a set of concept symbols Σ, that is referred to as the forgetting vocabulary. A description logic to first-order logic translator that uses the established relationship between them [1] has been built. The tool uses the translator to translate an ontology expressed in OWL syntax to an equivalent set of first-order formulae expressed in Otter syntax. It is used to translate the input ontology into an equivalent input for SCAN. After each of the two systems have computed its solution, a first-order logic theorem prover called Prover91 was used to check for entailments between the results. The translator was used again to translate LETHE's results to first-order logic as Prover9 uses the Otter syntax, too.
The system shown in Figure 2 is another version of the one used in Figure 1, except that the appropriate changes were made to use FAME instead of SCAN.
In this section, the results of the comparison made between the solutions produced using SCAN and LETHE are presented. Following this, the results of the comparison made between the solutions produced using LETHE and FAME are presented in the next section.
In both comparisons, a set of randomly selected concepts was forgotten. The cardinality of the forgetting vocabulary varied depending on the number of concepts present in the ontology. However, for each ontology, an effort has been made to test and evaluate the forgetting solutions computed, as a result of forgetting sets of concepts of different sizes, ranging from low to high. In ontologies expressed in description logics that are more expressive than description logic ALC, an ALC fragment of the ontologies were used. The tests where LETHE produces results that contain definer symbols were excluded as they are not part of the original vocabulary.
After testing and evaluating fragments of different ontologies from the OBO Foundry ontology repository2 , the following results were observed.
1. The solutions computed using SCAN always entail the solutions computed using LETHE. 2. The solutions computed using LETHE always entail the solutions computed using SCAN if no Skolem terms occur in SCAN's solutions. However, if Skolem terms do occur in the solution, the solution computed using LETHE entail the subset of clauses and formulas that do not contain Skolem terms. 3. In some cases, the subset of clauses and formulas in SCAN's solution, that do not contain Skolem terms, is sufficient to entail the forgetting solutions computed using LETHE. The exact reason behind this occurrence raises interesting new questions of research. 4. If SCAN and LETHE both terminate, the approach used to develop SCAN outperforms the approach used to develop LETHE. However, it must be noted that this is the average situation. 5. In some cases the two approaches agree on the difficulty of the forgetting problem. However, in other cases, it was observed that LETHE found some forgetting problems to be difficult, while SCAN found a solution relatively quickly. It was speculated that the reverse occurs as well, but currently there is not sufficient evidence to support it.
Based on the testing and evaluation performed using fragments of ontologies from the Oxford ontology repository3 , the following results were observed:
1. If FAME successfully forgets all the symbols in the forgetting vocabulary and produces a solution that is expressed in description logic ALC, rather than a more expressive description logic such as ALCI, then the solutions produced by FAME and LETHE entail one another. 2. If FAME successfully forgets all the symbols in the forgetting vocabulary, but produces a solution in a more expressive description logic, namely ALCI, then the solutions produced by FAME entail those produced by LETHE. 3. If FAME fails to forget a subset of the forgetting vocabulary and LETHE produces a solution that does not contain any unwanted symbols such as definer symbols, then the solutions produced by FAME entail those produced by LETHE. This case captures the strength of resolution as it shows that there exist cases where a forgetting problem can be solved using resolution but not using an Ackermann-based approach. Consequently, this opens the door to consider a hybrid technique that benefits from the speed of FAME and the power of LETHE.
4. One of the differences between FAME and LETHE is that LETHE introduces definer symbols using standard flattening techniques to structurally transform the ontology into what is called normal form, in order to simplify its computations. We found that if LETHE introduces definer symbols and fails to eliminate all of them, FAME fails to forget at least one symbol in the ontology. Consequently, if FAME fails to forget at least one symbol and LETHE fails to eliminate at least one definer symbol, then no entailments can be inferred. This is obvious because each tool produces solutions that contain symbols that are not present in the solutions of the other tool. However, interestingly, one of the flattening techniques used to produce definer symbols in LETHE is inspired by Ackermann's Lemma; instead of using the Lemma to eliminate a symbol, it is used to introduce one. Hence, this raises the question: what is the relationship between the definer symbols that LETHE failed to eliminate and the symbols FAME failed to forget? We expect that these are cases of symbols with cyclic dependencies, which remains to be checked.
Parts of the theory were confirmed and verified using a tool that was developed for the purposes of this research. The tool aims to compare the solutions computed using the three forgetting tools: SCAN, LETHE and FAME. It provided insight into the relationship between the three forgetting tools in the absence of a theoretical comparison. The possibilities of a hybrid system are currently being investigated in an attempt to improve the performance while exploiting the power of resolution. A naive implementation has shown interesting results, particularly, for one of the forgetting problems. This problem took the resolution rules, implemented in LETHE, more than 14 hours to compute a solution. On the other hand, FAME, which exploits Ackermann's Lemma, successfully forgets all the symbols in the forgetting problem, except for one, in two seconds. The hybrid method which first applies FAME and then LETHE to the result computed by FAME successfully forgets all the symbols in the forgetting problem in three seconds. It would be interesting to develop heuristics that select the approach to use for each symbol in the forgetting vocabulary.
Moreover, we are interested in investigating the relationships between the tools and the underlying approaches more deeply. For example, we have not yet found any counterexamples to the following statement: when FAME successfully forgets all the symbols in the forgetting vocabulary, but produces results in ALCI, we have that the solutions produced by LETHE entail a subset of those produced by FAME, namely the subset of solutions that are expressed in description logic ALC. Additionally, no cases where FAME successfully forgets all the symbols and LETHE fails to eliminate a definer symbol were found during this research. We would like to investigate if this can theoretically happen. For concept forgetting in ALC, we expect that this cannot happen. Finally, we would like to continue investigating the relationship between the approaches used in the various systems but for more expressive description logics.