LETHE: Forgetting and Uniform Interpolation for Expressive Description Logics
- PDF / 1,704,980 Bytes
- 7 Pages / 595.276 x 790.866 pts Page_size
- 11 Downloads / 215 Views
SYSTEMS DESCRIPTION
LETHE: Forgetting and Uniform Interpolation for Expressive Description Logics Patrick Koopmann1 Received: 30 December 2019 / Accepted: 25 March 2020 © The Author(s) 2020
Abstract Uniform interpolation and forgetting describe the task of projecting a given ontology into a user-specified vocabulary, that is, of computing a new ontology that only uses names from a specified set of names, while preserving all logical entailments that can be expressed with those names. This is useful for ontology analysis, ontology reuse and privacy. Lethe is a tool for performing uniform interpolation on ontologies in expressive description logics, and it can be used from the command line, using a graphical interface, and as a Java library. It furthermore implements methods for computing logical difference and performing abduction using uniform interpolation. We present the tool together with an evaluation on a varied corpus of realistic ontologies. Keywords Description logics · Non-classical reasoning · Uniform interpolation · Forgetting
1 Introduction Description logic (DL) ontologies are used in a range of application areas as a means to define terminological domain knowledge via concept and role names. Applications in medicine, biology and the semantic web often lead to the development of large and complex ontologies that cover wide areas of knowledge. Understanding and maintaining such complex ontologies becomes difficult without appropriate tool support. On the other hand, some information from existing ontologies might be useful for reuse in new ontologies, while one does not want to import the complexity of the whole ontology. Uniform interpolation, also studied under the name of forgetting, has the potential to approach these challenges [4, 14]. Given an ontology O and a signature 𝛴 of concept and role names, a uniform interpolant for O over 𝛴 is a new ontology that covers all logical entailments in 𝛴 , while using no names that are outside of the signature 𝛴 (see Fig. 1 for an example). Uniform interpolation Funded by the DFG grant 389793660 as part of TRR 248 (see https://www.perspicuous-computing.science/) * Patrick Koopmann patrick.koopmann@tu‑dresden.de 1
Institute of Theoretical Computer Science, Technische Universität Dresden, 01187 Dresden, Germany
can be used for ontology reuse by computing a specialised ontology that only deals with the names that are relevant for the new application. Furthermore, it can be used to make implicit, hidden relations between names visible, which can be helpful for ontology understanding and maintenance. In addition, uniform interpolation can be used to solve other non-classical reasoning problems relevant in the context of ontology maintenance, such as logical difference [19] and abduction [3, 15]. Lethe is a tool that can be used to compute uniform interpolants in different expressive DLs.1 Internally, it uses a resolution method presented in [9] for ALCH TBoxes, and later extended to SHQ [10] and knowledge bases consisting of both a TBox and an ABox [
Data Loading...
