Forgetting eliminates symbols from a knowledge base so that consequences over the remaining symbols in the signature are preserved. In logic the problem has been studied as the uniform interpolation problem. Uniform interpolation is a notion related to the Craig interpolation problem, but is stronger. In computer science the importance of forgetting can be found in the knowledge representation literature, specification refinement literature and the area of description logic-based ontology engineering. In ontology-based information processing, forgetting allows users to focus on specific parts of ontologies in order to create decompositions and restricted views for in depth analysis or sharing with other users. Forgetting is also useful for information hiding, explanation generation, semantic difference computation and ontology debugging. Forgetting is an inherently difficult problem, much harder than standard reasoning (satisfiability and validity testing), and very few logics are known to be complete for forgetting (or have the uniform interpolation property). These not so encouraging premises should however not prevent us from developing practical methods for computing forgetting solutions and uniform interpolants. My presentation gives an overview of the methods and success stories of three forgetting tools: - Scan, which performs second-order quantifier elimination [1, 2], - Lethe, which solves the uniform interpolation problem for many expressive description problems extending ALC [3, 4], and - Fame, which computes semantic forgetting solutions for description logics of different expressivity [5, 6].
Copyright c 2017 by the paper's authors