Servicenavigation

Project Details

Back

Projekt Print View

Live Ontologies - Reasoning Support for the Development of Distributed and Dynamically Changing OWL Ontologies

Subject Area Theoretical Computer Science
Image and Language Processing, Computer Graphics and Visualisation, Human Computer Interaction, Ubiquitous and Wearable Computing
Term from 2011 to 2018
Project identifier Deutsche Forschungsgemeinschaft (DFG) - Project number 203848550
 
Final Report Year 2019

Final Report Abstract

Logic-based ontology languages, such as OWL, are increasingly used in applications to define and work with expert knowledge from diverse domains, such as biology, medicine, or engineering. The development of large ontologies is a complex process that involves a collaboration of multiple ontology developers over extended periods of time. Just like in Software Engineering, ontology developers use editors and tools that simplify the editing workflow and help preventing typical errors. Ontology reasoners are one of such tools. They can be used to automatically check consistency of ontologies and answer queries about the knowledge implied by the ontologies. This project focuses on the development of ontology reasoning procedures that can work incrementally over ontology changes, modular over distributed ontologies, and provide easy to understand explanations for the reasoning results to ontology developers. In the second phase of the project, covered by this report, we have obtained new results on distributed ontology reasoning and developed several applications for ontology debugging. Just like in Software Development, ontologies are rarely developed from scratch, but rather built from existing ontologies. In OWL this is possible by implicitly including content of other ontologies using import declarations. This way one can create complex networks of distributed ontologies. Reasoning with distributed ontologies is, however, difficult since the effect of imports is not local: the reasoner must take into account all axioms of (possibly indirectly) imported ontologies, which could be a very large set. In contrast, typical applications usually require only a small number of terms from the imported ontologies. In this project, we have defined a new, semantic, ontology import mechanism, using which only the logical consequences over a specified vocabulary of symbols is imported from existing ontologies. This is similar to the use of programming libraries, which expose functionality through a restricted set of application interfaces. The main goal was the development of distributed ontology reasoning procedures, whereby reasoning is performed by exchanging of relevant logical consequences between ontologies. Towards this goal, we have studied the expressive power of semantic import relations for different ontology languages, and came to a surprising conclusion that the standard reasoning problems become undecidable already for languages, for which reasoning without imports is tractable. The undecidability result is obtained using ontologies with cyclic semantic import relations, which augment languages with a certain form of recursion. But even when restricted the import relations to be acyclic, we showed that reasoning in ontology networks becomes exponentially harder for most of the commonly used languages. The main outcome of these results is that semantic importing gives a new expressivity to ontology languages, which, consequently, increases the worst-case complexity of reasoning. The second outcome of the project is the development of new methods and tools for ontology debugging. In the first phase of the project, we have developed a goal-directed procedure for generation of proofs using a deductive closure of an ontology. In the second phase, we used these proofs in newly developed plugins for the ontology editor Protege. The Proof Explanation plugin allows an ontology developer to inspect proofs for an entailment of interest. To improve understanding of proofs, we have implemented several proof simplification strategies. For example, we filter out cyclic inferences, remove unnecessary axioms and tautologies, and combine nested inferences into one. These proof transformations guarantee to preserve proof completeness: if it was possible to derive an entailment in the original proof from a subset of axioms, then it is also possible to do so after the transformation. Complete proofs have a nice property that they represent all justifications for the entailment—minimal subset of axioms which entail the given logical conclusion. In our next contribution, we have developed a new resolution-based procedures, using which all such justifications can be efficiently enumerated. Our procedure has some unique advantages compared to other procedures for enumeration of justifications, which use propositional SAT solvers. For example, one can enumerate justification in any desirable order. We have implemented and optimized our procedure, and obtained some very encouraging experimental results. For example, we have been able, for the first time, to compute all justifications for the reasoning results in one of the largest and widely used medical ontologies Snomed CT. We have further developed several Protege plugins that can display such justifications to ontology developers. The outcomes of the project were published in workshop and conference publications, and the software was made available in open source tools and libraries. Out tools, such as the ELK reasoner, developed in the fist phase of the project, are already used in multiple research and commercial projects, such as in the development of the widely used Gene Ontology and Snomed CT. We are confident that the new outcomes of the projects will be also used in these settings.

Publications

 
 

Additional Information

© 2025 DFG Disclaimer / Copyright / Privacy Policy

Textvergrößerung und Kontrastanpassung