Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

Live Ontologien - Unterstützung von automatischem Schlussfolgern in der Entwicklung von verteilten und sich ändernden OWL Ontologien

Antragsteller Dr. Yevgeny Kazakov
Fachliche Zuordnung Theoretische Informatik
Bild- und Sprachverarbeitung, Computergraphik und Visualisierung, Human Computer Interaction, Ubiquitous und Wearable Computing
Förderung Förderung von 2011 bis 2018
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 203848550
 
Erstellungsjahr 2019

Zusammenfassung der Projektergebnisse

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.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2025 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung