Live Ontologien - Unterstützung von automatischem Schlussfolgern in der Entwicklung von verteilten und sich ändernden OWL Ontologien
Bild- und Sprachverarbeitung, Computergraphik und Visualisierung, Human Computer Interaction, Ubiquitous und Wearable Computing
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)
- Incremental reasoning in OWL EL without bookkeeping. In Harith Alani et al., editors, Proc. 12th Int. Semantic Web Conf. (ISWC’13), volume 8218 of Lecture Notes in Computer Science, pages 232–247. Springer, 2013
Yevgeny Kazakov and Pavel Klinov
(Siehe online unter https://doi.org/10.1007/978-3-642-41335-3_15) - Bridging the gap between tableau and consequencebased reasoning. In Meghyn Bienvenu, Magdalena Ortiz, Riccardo Rosati, and Mantas Simkus, editors, Proc. 27th Int. Workshop on Description Logics (DL’14), volume 1193 of CEUR Workshop Proceedings, pages 579–590. CEUR-WS.org, 2014
Yevgeny Kazakov and Pavel Klinov
- Goal-directed tracing of inferences in EL ontologies. In Peter Mika et al., editors, Proc. 13th Int. Semantic Web Conf. (ISWC’14), volume 8796 of Lecture Notes in Computer Science, pages 196–211. Springer, 2014
Yevgeny Kazakov and Pavel Klinov
(Siehe online unter https://doi.org/10.1007/978-3-319-11915-1_13) - The incredible ELK: From polynomial procedures to efficient reasoning with EL ontologies. J. of Automated Reasoning, 53(1):1–61, 2014
Yevgeny Kazakov, Markus Krötzsch, and Frantisek Simancik
(Siehe online unter https://doi.org/10.1007/s10817-013-9296-3) - Advancing ELK: not only performance matters. In Diego Calvanese and Boris Konev, editors, Proc. 28th Int. Workshop on Description Logics (DL’15), volume 1350 of CEUR Workshop Proceedings. CEUR-WS.org, 2015
Yevgeny Kazakov and Pavel Klinov
- Enumerating justifications using resolution. In Alessandro Artale, Birte Glimm, and Roman Kontchakov, editors, Proc. 30th Int. Workshop on Description Logics (DL’17), volume 1879 of CEUR Workshop Proceedings. CEUR-WS.org, 2017
Yevgeny Kazakov and Peter Skocovsky
- On the complexity of semantic integration of OWL ontologies. In Alessandro Artale, Birte Glimm, and Roman Kontchakov, editors, Proc. 30th Int. Workshop on Description Logics (DL’17), volume 1879 of CEUR Workshop Proceedings. CEUR-WS.org, 2017
Yevgeny Kazakov and Denis K. Ponomaryov
- Towards reusable explanation services in Protégé. In Alessandro Artale, Birte Glimm, and Roman Kontchakov, editors, Proc. 30th Int. Workshop on Description Logics (DL’17), volume 1879 of CEUR Workshop Proceedings. CEUR-WS.org, 2017
Yevgeny Kazakov, Pavel Klinov, and Alexander Stupnikov
- Applying a model of text comprehension to automated verbalizations of EL derivations. In Magdalena Ortiz and Thomas Schneider, editors, Proc. 31st Int. Workshop on Description Logics (DL’18), volume 2211 of CEUR Workshop Proceedings. CEUR-WS.org, 2018
Tanja Perleth, Marvin R. G. Schiller, and Birte Glimm
- Enumerating justifications using resolution. In Proc. 9th Int. Joint Conf. on Automated Reasoning (IJCAR’18), volume 10900 of Lecture Notes in Computer Science, pages 609–626. Springer, 2018
Yevgeny Kazakov and Peter Skocovsky
(Siehe online unter https://doi.org/10.1007/978-3-319-94205-6_40)
