Deductive Module Extraction for Expressive Description Logics

In deductive module extraction, we determine a small subset of an ontology for a given vocabulary that preserves all logical entailments that can be expressed in that vocabulary. While in the literature stronger module notions have been discussed, we argue that for applications in ontology analysis and ontology reuse, deductive modules, which are decidable and potentially smaller, are often sufficient. We present methods based on uniform interpolation for extracting different variants of deductive modules, satisfying properties such as completeness, minimality and robustness under replacements, the latter being particularly relevant for ontology reuse. An evaluation of our implementation shows that the modules computed by our method are often significantly smaller than those computed by existing methods.

LETHE: Forgetting and Uniform Interpolation for Expressive Description Logics

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.

Tracking Logical Difference in Large-Scale Ontologies: A Forgetting-Based Approach

This paper explores how the logical difference between two ontologies can be tracked using a forgetting-based or uniform interpolation (UI)-based approach. The idea is that rather than computing all entailments of one ontology not entailed by the other ontology, which would be computationally infeasible, only the strongest entailments not entailed in the other ontology are computed. To overcome drawbacks of existing forgetting/uniform interpolation tools we introduce a new forgetting method designed for the task of computing the logical difference between different versions of large-scale ontologies. The method is sound and terminating, and can compute uniform interpolants for ALC-ontologies as large as SNOMED CT and NCIt. Our evaluation shows that the method can achieve considerably better success rates (>90%) and provides a feasible approach to computing the logical difference in large-scale ontologies, as a case study on different versions of SNOMED CT and NCIt ontologies shows.

ABox Abduction via Forgetting in ALC

Abductive reasoning generates explanatory hypotheses for new observations using prior knowledge. This paper investigates the use of forgetting, also known as uniform interpolation, to perform ABox abduction in description logic (ALC) ontologies. Non-abducibles are specified by a forgetting signature which can contain concept, but not role, symbols. The resulting hypotheses are semantically minimal and consist of a disjunction of ABox axioms. These disjuncts are each independent explanations, and are not redundant with respect to the background ontology or the other disjuncts, representing a form of hypothesis space. The observations and hypotheses handled by the method can contain both atomic or complex ALC concepts, excluding role assertions, and are not restricted to Horn clauses. Two approaches to redundancy elimination are explored in practice: full and approximate. Using a prototype implementation, experiments were performed over a corpus of real world ontologies to investigate the practicality of both approaches across several settings.

Uniform interpolation for propositional and modal team logics

In this paper we consider modal team logic, a generalization of classical modal logic in which it is possible to describe dependence phenomena between data. We prove that most known fragments of full modal team logic allow the elimination of the so called ‘existential bisimulation quantifiers’, where the existence of a certain set is required only modulo bisimulation (i.e. not in the model itself but possibly in a bisimilar model). As a consequence, we prove that these fragments enjoy the uniform interpolation property.