Logical Methods for Ontology Engineering
Image and Language Processing, Computer Graphics and Visualisation, Human Computer Interaction, Ubiquitous and Wearable Computing
Final Report Abstract
To process information in an intelligent way, it is necessary to represent relevant knowledge so that it can be understood not only by humans but also by computers. Logic-based ontology languages, such as OWL make this possible by formally specifying which information implicitly follows from the knowledge described by means of ontological axioms. This way, ontologies can be developed by domain experts similarly to software. Just like in software development, ontology development is a error-prone process. This project focuses on development of logic-based methods and tools that can help developing hight quality ontologies. The central part of such tools are ontology reasoners. These are programs that can automatically compute logical consequences of ontologies, e.g., to verify correctness of the information and answer user queries. The first outcome of the project are new methods and tools for ontology debugging. In the first phase of the project, we have developed general goal-directed procedure for generation of proofs for ontological entailments. 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. The plugin includes several proof simplification strategies to improve understanding of proofs. It is also common to explain the ontological entailments using justifications—minimal subset of axioms that 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 developed several Protege plugins that can display such justifications to ontology developers. The second outcome of the project are new complexity results for reasoning with distributed ontologies. Just like in software development, ontologies are rarely developed from scratch, but rather built from existing ontologies. 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. 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 restricting 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 expressive power to ontology languages, which, consequently, increases the worst-case complexity of reasoning. 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 first 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
- 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
(See online at https://doi.org/10.1007/978-3-642-41335-3_15) - Bridging the gap between tableau and consequencebased reasoning. In Meghyn Bienvenu et al., 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
(See online at 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
(See online at 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
(See online at https://doi.org/10.1007/978-3-319-94205-6_40)
