Forgetting refers to an ontology engineering technique that seeks to produce new ontologies from existing ones using only a subset of their signature while preserving all logical consequences up to the names in the subset. This can be done by eliminating from the original ontology a set of concept and role names in such a way that all logical consequences are preserved up to the names in the remaining signature. The ontology produced by forgetting, namely the forgetting solution, can be seen as a view of the original ontologies. In traditional databases, a view is a subset of the database, whereas in ontologies, a view is more than a subset; it may contain not only axioms contained in the ontology, but also those entailed by the ontology (implicitly contained in the ontology). Forgetting has a number of potential applications such as ontology reuse, versioning, alignment, merging, debugging, repair, and logical di erence computation [1,12,16,3,14,5,2,17,2]. Forgetting can be de ned as the dual of uniform interpolation [15] or modeltheoretically as semantic forgetting [5,20,4]. The two notions di er in the sense that uniform interpolation preserves all logical consequences up to certain signatures while semantic forgetting preserves semantic equivalence up to certain signatures. The results of semantic forgetting (the semantic solutions ), are in general stronger than those of uniform interpolation (the uniform interpolants ). This means that semantic solutions always entail uniform interpolants, but the converse does not hold. Uniform interpolants are always expressed in the source logic, while semantic solutions are often not expressible in the source logic, and may require the target language to be extended. Practical methods for computing uniform interpolants include the method implemented in the Lethe system [7,8,9,11], and the method developed by [13]. Lethe handles ALC, ALCH, SIF , SHQ-TBoxes, and ALC with ABoxes. The method of [13] handles ALC-TBoxes. Practical methods for computing semantic solutions of forgetting have been developed, implemented and evaluated in work of [18,19]. These methods are based on non-trivial generalisations of Ackermann's Lemma, and attempt to eliminate concept and role names from ontologies expressible in the description logic ALCOIH(O; u). This paper introduces a practical method for computing solutions of concept forgetting in description logics with quali ed number restrictions. While allowing more problems to be solved, admitting quali ed number restrictions signi cantly increases the di culty of the problem. Our method handles in particular ? This is an extended abstract of a paper published in the proceedings of IJCAI 2018.
ALCOQ-ontologies and the extension with the universal role, role negation, role conjunction and role disjunction, which means that it can handle expressive description logics that cannot be handled by other methods at present. The method is terminating, sound, but incomplete for ALCOQ(:; u; t)-ontologies. When it succeeds, the method returns a uniform interpolant in ALCOQ(:; u; t). The results of an evaluation with a prototype implementation shows that the method is computationally feasible and is able to nd a uniform interpolant in more than 90% of the test cases taken from a large corpus of biomedical ontologies. In only 13.2% of these cases the uniform interpolant was also a semantic solution. The prototype, along with the test ontologies and their statistical information, can be downloaded/found at http://www.cs.man.ac.uk/~schmidt/sf-fame/.
At present, practical methods for forgetting in description logics with
quali ed number restrictions are the resolution-based approach of the Lethe
system [
5(hasSon t hasDaughter):>; where role disjunction is used. Upon the solution of Lethe, if we further forget the role names hasSon and hasDaughter, the uniform interpolant is fA v 3hasChild:>g, while upon the intermediary solution of the prototype, the solution is fA v 5hasChild:>g, which is stronger and closer to the fact: A has at least 5 children. This shows an advantage of our method where extra expressivity allows intermediary information (A v 5(hasSon t hasDaughter):>) to be captured which produces a better solution.