Tableau-based Forgetting in 𝒜ℒ𝒞 Ontologies

In this paper, we propose two new approaches to forgetting for 𝒜ℒ𝒞 based on the well-known tableau algorithm. The first approach computes the result of forgetting by rolling up tableaux, and also provides a decision algorithm for the existence of forgetting in 𝒜ℒ𝒞. When the result of forgetting does not exist, we provide an incremental method for computing approximations of forgetting. This second approach uses variable substitution to refine approximations of forgetting and eventually obtain the result of forgetting. This approach is capable of preserving structural information of the original ontologies enabling readability and comparison. As both approaches are based on the tableau algorithm, their implementations can make use of the mechanisms and optimization techniques of existing description logic reasoners.