% % This file was created by the TYPO3 extension % publications % --- Timezone: CEST % Creation date: 2024-03-28 % Creation time: 21:54:11 % --- Number of references % 60 % @Inproceedings { GlKa22, author = {Glimm, Birte and Kazakov, Yevgeny}, title = {SAT-Based Axiom Pinpointing Revisited}, abstract = {Propositional SAT solvers have been a popular way of computing justifications for ontological entailment– minimal subsets of axioms of the ontologies that entail a given conclusion. Most SAT encodings proposed for Description Logics (DLs), translate the inferences obtained by a consequence-based procedure to propositional Horn clauses, using which entailments from subsets of axioms can be effectively checked, and use modified SAT solvers to systematically search over these subsets. To avoid repeated discovery of subsets with already checked entailment, the modified SAT solvers add special blocking clauses that prevent generating truth assignments corresponding to these subsets, the number of which can be exponential, even if the number of justifications is small. In this paper, we propose alternative SAT encodings that avoid generation of unnecessary blocking clauses. Unlike the previous methods, the inferences are used not only for checking entailment from subsets of axioms, but also, as a part of the encoding, to ensure that the SAT solver generates truth assignments corresponding only to justifications.}, year = {2022}, booktitle = {Proceedings of the 35th International Workshop on Description Logics (DL 2022)}, volume = {3263}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Ofer Arieli and Martin Homola and Jean Christoph Jung and Marie-Laure Mugnier}, file_url = {https://ceur-ws.org/Vol-3263/paper-10.pdf} } @Inproceedings { GlKW22, author = {Glimm, Birte and Kazakov, Yevgeny and Welt, Michael}, title = {Concept Abduction for Description Logics}, abstract = {We present two alternative algorithms for computing (all or some) solutions to the concept abduction problem: one algorithm is based on Reiter's hitting set tree algorithm, whereas the other one relies on a SAT encoding. In contrast to previous work, the algorithms do not rely on a refutation-based calculus and, hence, can be used also with efficient reasoners for tractable DLs such as \$\mathcalEL\$ and its extensions. An adaptation to other forms of (logic-based) abduction, e.g., to ABox abduction, is also possible. }, year = {2022}, booktitle = {Proceedings of the 35th International Workshop on Description Logics (DL 2022)}, volume = {3263}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Ofer Arieli and Martin Homola and Jean Christoph Jung and Marie-Laure Mugnier}, file_url = {https://ceur-ws.org/Vol-3263/paper-11.pdf} } @Inproceedings { DBLP:conf/rweb/GlimmK19, author = {Glimm, Birte and Kazakov, Yevgeny}, title = {Classical Algorithms for Reasoning and Explanation in Description Logics}, year = {2019}, DOI = {10.1007/978-3-030-31423-1\_1}, booktitle = {Reasoning Web. Explainable Artificial Intelligence - 15th International Summer School}, volume = {11810}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, editor = {Markus Kr\"{o}tzsch and Daria Stepanova}, pages = {1-64}, tags = {KnowledgeModeling}, web_url = {https://doi.org/10.1007/978-3-030-31423-1\\_1}, file_url = {t3://file?uid=420338} } @Conference { KazSko:IJCAR18:Justifications, author = {Kazakov, Yevgeny and Skocovsky, Peter}, title = {Enumerating Justifications using Resolution}, abstract = {If a conclusion follows from a set of axioms, then its justification is a minimal subset of axioms for which the entailment holds. An entailment can have several justifications. Such justifications are commonly used for the purpose of debugging of incorrect entailments in Description Logic ontologies. Recently a number of SAT-based methods have been proposed that can enumerate all justifications for entailments in light-weight ontologies languages, such as EL. These methods work by encoding EL inferences in propositional Horn logic, and finding minimal models that correspond to justifications using SAT solvers. In this paper, we propose a new procedure for enumeration of justifications that uses resolution with answer literals instead of SAT solvers. In comparison to SAT-based methods, our procedure can enumerate justifications in any user-defined order that extends the set inclusion relation. The procedure is easy to implement and, like resolution, can be parametrized with ordering and selection strategies. We have implemented this procedure in PULi - a new Java-based Proof Utility Library, and performed an empirical comparison of (several strategies of) our procedure and other SAT-based tools on popular EL ontologies. The experiments show that our procedure provides a comparable, if not better performance than those highly optimized tools. For example, using one of the strategies, we were able for the first time to compute all justifications for all entailed concept subsumptions in one of the largest commonly used medical ontology Snomed CT.}, year = {2018}, isbn = {978-3-319-94204-9}, DOI = {10.1007/978-3-319-94205-6}, booktitle = {IJCAR}, volume = {10900}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, editor = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani}, pages = {609--626}, tags = {KnowledgeModeling LiveOntologies}, web_url = {https://doi.org/10.1007/978-3-319-94205-6\_40}, file_url = {/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2018/KazSko18Justifications\_IJCAR.pdf} } @Inproceedings { KazSko:DL17:Justifications, author = {Kazakov, Yevgeny and Skocovsky, Peter}, title = {Enumerating Justifications using Resolution}, abstract = {We propose a new procedure that can enumerate justifications of a logical entailment given a set of inferences using which this entailment can be derived from axioms in the ontology. The procedure is based on the extension of the resolution method with so-called answer literals. In comparison to other (SAT-based) methods for enumerating justifications, our procedure can enumerate justifications in any user-defined order that extends the subset relation. The procedure is easy to implement and can be parametrized with ordering and selection strategies used in resolution. We describe an implementation of the procedure provided in PULi--a new Java-based Proof Utility Library, and provide an em- pirical comparison of (several strategies of) our procedure and other SAT-based tools on popular EL ontologies. The experiments show that our procedure provides a comparable, if not better performance than those highly optimized tools. For example, using one of the strategies, we were able to compute all justifications for all direct subsumptions of Snomed CT in about 1.5 hour. No other tool used in our experiments was able to do it even within a much longer period. }, year = {2017}, booktitle = {Proceedings of the 30th International Workshop on Description Logics (DL 2017)}, volume = {1879}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Alessandro Artale and Birte Glimm and Roman Kontchakov}, tags = {KnowledgeModeling, LiveOntologies}, web_url = {http://ceur-ws.org/Vol-1879/paper38.pdf}, file_url = {/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2017/KazSko17Justifications\_DL.pdf} } @Inproceedings { KazPon:DL17:Integration, author = {Kazakov, Yevgeny and Ponomaryov, Denis}, title = {On the Complexity of Semantic Integration of OWL Ontologies}, abstract = {We propose a new mechanism for integration of OWL ontologies using semantic import relations. In contrast to the standard OWL importing, we do not require all axioms of the imported ontologies to be taken into account for reasoning tasks, but only their logical implications over a chosen signature. This property comes natural in many ontology integration scenarios. In this paper, we study the complexity of reasoning over ontologies with semantic import relations and establish a range of tight complexity bounds for various fragments of OWL.}, year = {2017}, booktitle = {Proceedings of the 30th International Workshop on Description Logics (DL 2017)}, volume = {1879}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Alessandro Artale and Birte Glimm and Roman Kontchakov}, tags = {KnowledgeModeling, LiveOntologies}, web_url = {http://ceur-ws.org/Vol-1879/paper59.pdf}, file_url = {/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2017/KazPon17Integration\_DL.pdf} } @Conference { GliKazTra:17:Abstraction:Horn:SHOIF:AAAI, author = {Glimm, Birte and Kazakov, Yevgeny and Tran, Trung-Kien}, title = {Ontology Materialization by Abstraction Refinement in Horn SHOIF}, abstract = {Abstraction refinement is a recently introduced technique using which reasoning over large ABoxes is reduced to reasoning over small abstract ABoxes. Although the approach is sound for any classical Description Logic such as \{SROIQ\}, it is complete only for Horn \{ALCHOI\}. In this paper, we propose an extension of this method that is now complete for Horn \{SHOIF\} and also handles role- and equality-materialization. To show completeness, we use a tailored set of materialization rules that loosely decouple the ABox from the TBox. An empirical evaluation demonstrates that, despite the new features, the abstractions are still significantly smaller than the original ontologies and the materialization can be computed efficiently.}, year = {2017}, booktitle = {Proceedings of the 31st AAAI Conference on Artificial Intelligence}, publisher = {AAAI Press}, editor = {Satinder P. Singh and Shaul Markovitch}, pages = {1114--1120}, event_name = {31st AAAI Conference on Artificial Intelligence}, event_place = {San Francisco, California, USA}, tags = {AutomatedReasoning}, web_url = {http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14726}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2017/GlKT17a.pdf} } @Inproceedings { GlKT17b, author = {Glimm, Birte and Kazakov, Yevgeny and Tran, Trung-Kien}, title = {Scalable Reasoning by Abstraction in DL-Lite}, year = {2017}, booktitle = {Proceedings of the 30th International Workshop on Description Logics (DL 2017)}, volume = {1879}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, tags = {AutomatedReasoning}, web_url = {http://ceur-ws.org/Vol-1879/paper57.pdf}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2017/GlKT17b.pdf} } @Inproceedings { KazKliStu:DL17:Explanations, author = {Kazakov, Yevgeny and Klinov, Pavel and Stupnikov, Alexander}, title = {Towards Reusable Explanation Services in Protege}, abstract = {We present several extensions of the explanation facility of the ontology editor Protege. Currently, explanations of OWL entailments in Protege are provided as justifications--minimal subsets of axioms that entail the given axiom. The plugin called \grqexplanation workbench’ computes justifications using a black-box algorithm and displays them in a convenient way. Recently, several other (mostly glass-box) tools for computing justifications have been developed, and it would be of interest to use such tools in Protege. To facilitate the development of justification-based explanation plugins for Protege, we have separated the explanation workbench into two reusable components--a plugin for black- box computation of justifications and a plugin for displaying (any) justifications. Many glass-box methods compute justifications from proofs, and we have also developed a reusable plugin for this service that can be used with (any) proofs. In addition, we have developed an explanation plugin that displays such proofs directly. Both plugins can be used, e.g., with the proofs provided by the ELK reasoner. This paper describes design, features, and implementation of these plugins.}, year = {2017}, booktitle = {Proceedings of the 30th International Workshop on Description Logics (DL 2017)}, volume = {1879}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Alessandro Artale and Birte Glimm and Roman Kontchakov}, tags = {KnowledgeModeling, ELK, LiveOntologies}, web_url = {http://ceur-ws.org/Vol-1879/paper31.pdf}, file_url = {/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2017/KazKliStu17Explanations\_DL.pdf} } @Inproceedings { GlKT16a, author = {Glimm, Birte and Kazakov, Yevgeny and Tran, Trung-Kien}, title = {Ontology Materialization by Abstraction Refinement in Horn SHOIF}, year = {2016}, booktitle = {Proceedings of the 29th International Workshop on Description Logics (DL 2016)}, volume = {1577}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, tags = {AutomatedReasoning}, web_url = {http://ceur-ws.org/Vol-1577/invited\_paper\_1.pdf}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2016/GlKT16a.pdf} } @Inproceedings { GlKT16b, author = {Glimm, Birte and Kazakov, Yevgeny and Tran, Trung-Kien}, title = {Scalable Reasoning by Abstraction Beyond DL-Lite}, year = {2016}, booktitle = {Proceedings of the 10th International Conference on Web Reasoning and Rule Systems (RR 2016)}, volume = {9898}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, editor = {Magdalena Ortiz and Stefan Schlobach}, pages = {77--93}, keywords = {Reasoning, Description Logics, Optimisations, Optimizations, Materialization, Materialisation, Abstraction}, tags = {AutomatedReasoning}, web_url = {http://dx.doi.org/10.1007/978-3-319-45276-0\_7}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2016/GlKT16b.pdf}, note = {Best Student Paper Award} } @Inproceedings { KazKli:2015:Advancing-ELK:DL, author = {Kazakov, Yevgeny and Klinov, Pavel}, title = {Advancing ELK: Not Only Performance Matters}, abstract = {This paper reports on the recent development of ELK, a consequence-based reasoner for \$\mathcal\{EL^+\_\bot\}\$ ontologies. It covers novel reasoning techniques which aim at improving efficiency and providing foundation for new reasoning services. On the former front we present a simple optimization for handling of role composition axioms, such as transitivity, which substantially reduces the number of rule applications. For the latter, we describe a new rule application strategy that takes advantage of concept definitions to avoid many redundant inferences without making rules dependent on derived conclusions. This improvement is not visible to the end user but considerably simplifies implementation for incremental reasoning and proof generation. We also present a rewriting of low-level inferences used by ELK to higher-level proofs that can be defined in the standard DL syntax, and thus be used for automatic verification of reasoning results or (visual) ontology debugging. We demonstrate the latter capability using a new ELK Prot\'eg\'e plugin.}, year = {2015}, booktitle = {DL}, volume = {1350}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Diego Calvanese and Boris Konev}, tags = {KnowledgeModeling, ELK, LiveOntologies}, web_url = {http://ceur-ws.org/Vol-1350/paper-27.pdf}, file_url = {/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2015/KazKli15Advancing-ELK\_DL.pdf} } @Inproceedings { GKKS15b, author = {Glimm, Birte and Kazakov, Yevgeny and Kollia, Ilianna and Stamou, Giorgos}, title = {Lower and Upper Bounds for SPARQL Queries over OWL Ontologies}, year = {2015}, booktitle = {Proceedings of the 28th International Workshop on Description Logics (DL 2015)}, publisher = {CEUR Workshop Proceedings}, keywords = {Description Logics, Query Answering, Semantic Web, SPARQL}, tags = {AutomatedReasoning}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2015/GKKS15a.pdf} } @Inproceedings { GKKS14a, author = {Glimm, Birte and Kazakov, Yevgeny and Kollia, Ilianna and Stamou, Giorgos}, title = {Lower and Upper Bounds for SPARQL Queries over OWL Ontologies}, year = {2015}, booktitle = {Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI 2015)}, publisher = {AAAI Press}, keywords = {Description Logics, Query Answering, Semantic Web, SPARQL}, tags = {AutomatedReasoning}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2015/GKKS15a.pdf} } @Inproceedings { KazKli:14:ELK:Tracing:ISWC, author = {Kazakov, Yevgeny and Klinov, Pavel}, title = {Goal-Directed Tracing of Inferences in EL Ontologies}, abstract = {EL is a family of tractable Description Logics (DLs) that is the basis of the OWL 2 EL profile. Unlike for many expressive DLs, reasoning in EL can be performed by computing a deductively-closed set of logical consequences of some specific form. In some ontology-based applications, e.g., for ontology debugging, knowing the logical consequences of the ontology axioms is often not sufficient. The user also needs to know from which axioms and how the consequences were derived. Although it is possible to record all inference steps during the application of rules, this is usually not done in practice to avoid the overheads. In this paper, we present a goal-directed method that can generate inferences for selected consequences in the deductive closure without re-applying all rules from scratch. We provide an empirical evaluation demonstrating that the method is fast and economical for large EL ontologies. Although the main benefits are demonstrated for EL reasoning, the method can be potentially applied to many other procedures based on deductive closure computation using fixed sets of rules.}, year = {2014}, booktitle = {ISWC}, volume = {8797}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {196--211}, tags = {KnowledgeModeling, ELK, LiveOntologies}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2014/KazKli14Tracing\_ISWC.pdf} } @Article { KazKroSim:14:ELK:JAR, author = {Kazakov, Yevgeny and Kr\"{o}tzsch, Markus and Siman\v{c}\'{i}k, Franti\v{s}ek}, title = {The Incredible ELK: From Polynomial Procedures to Efficient Reasoning with EL Ontologies}, abstract = {EL is a simple tractable Description Logic that features conjunctions and existential restrictions. Due to its favorable computational properties and relevance to existing ontologies, EL has become the language of choice for terminological reasoning in biomedical applications, and has formed the basis of the OWL EL profile of the Web ontology language OWL. This paper describes ELK - a high performance reasoner for OWL EL ontologies - and details various aspects from theory to implementation that make ELK one of the most competitive reasoning systems for EL ontologies available today.}, year = {2014}, DOI = {10.1007/s10817-013-9296-3}, journal = {JAR}, volume = {53}, pages = {1-61}, number = {1}, tags = {KnowledgeModeling, ELK, LiveOntologies}, file_url = {/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2014/KazKroSim13ELK\_JAR.pdf} } @Inproceedings { GKLT14a, author = {Glimm, Birte and Kazakov, Yevgeny and Liebig, Thorsten and Tran, Trung-Kien and Vialard, Vincent}, title = {Abstraction Refinement for Ontology Materialization}, year = {2014}, booktitle = {Proceedings of the 27th International Workshop on Description Logics (DL 2014)}, volume = {1193}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, pages = {180-195}, keywords = {Reasoning, Description Logics, Optimisations, Optimizations}, tags = {AutomatedReasoning}, web_url = {http://ceur-ws.org/Vol-1193/paper\_6.pdf}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2014/GKLT14a.pdf} } @Inproceedings { Kaz:Kli:2014:Tracing:DL, author = {Kazakov, Yevgeny and Klinov, Pavel}, title = {Goal-Directed Tracing of Inferences in EL Ontologies}, abstract = {EL is a family of tractable Description Logics (DLs) that is the basis of the OWL 2 EL profile. Unlike for many expressive DLs, reasoning in EL can be performed by computing a deductively-closed set of logical consequences of some specific form. In some ontology-based applications, e.g., for ontology debugging, knowing the logical consequences of the ontology axioms is often not sufficient. The user also needs to know from which axioms and how the consequences were derived. Although it is possible to keep track of all inferences applied during reasoning, this is usually not done in practice to avoid the overheads. In this paper, we present a goal-directed method that can generate inferences for selected consequences in the deductive closure without re-applying all rules from scratch. We provide an empirical evaluation demonstrating that the method is fast and economical for large EL ontologies. Although the main benefits are demon- strated for EL reasoning, the method can be easily extended to other procedures based on deductive closure computation using fixed sets of rules.}, year = {2014}, booktitle = {DL}, volume = {1193}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Meghyn Bienvenu and Magdalena Ortiz and Riccardo Rosati and Mantas Simkus}, pages = {221-232}, tags = {KnowledgeModeling, ELK, LiveOntologies}, web_url = {http://ceur-ws.org/Vol-1193/paper\_26.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2014/KazKli14Tracing\_DL.pdf} } @Inproceedings { KazKli:2014:Tableau-CB:DL, author = {Kazakov, Yevgeny and Klinov, Pavel}, title = {Bridging the Gap between Tableau and Consequence-Based Reasoning}, abstract = {We present a non-deterministic consequence-based procedure for the description logic ALCHI. Just like the similar style (deterministic) procedures for EL and Horn-SHIQ, our procedure explicitly derives subsumptions between concepts, but due to non-deterministic rules, not all of these subsumptions are consequences of the ontology. Instead, the consequences are only those subsumptions that can be derived regardless of the choices made in the application of the rules. This is similar to tableau-based procedures, for which an ontology is inconsistent if every expansion of the tableau eventually results in a clash. We report on a preliminary experimental evaluation of the procedure using a version of SNOMED CT with disjunctions, which demonstrates some promising potential.}, year = {2014}, booktitle = {DL}, volume = {1193}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Meghyn Bienvenu and Magdalena Ortiz and Riccardo Rosati and Mantas Simkus}, pages = {579-590}, tags = {KnowledgeModeling, ELK, LiveOntologies}, web_url = {http://ceur-ws.org/Vol-1193/paper\_10.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2015/KazKli15Advancing-ELK\_DL.pdf} } @Inproceedings { GKLT14b, author = {Glimm, Birte and Kazakov, Yevgeny and Liebig, Thorsten and Tran, Trung-Kien and Vialard, Vincent}, title = {Abstraction Refinement for Ontology Materialization}, year = {2014}, DOI = {10.1007/978-3-319-11915-1\_12}, booktitle = {Proceedings of the 13th International Semantic Web Conference (ISWC 2014)}, volume = {8797}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, pages = {180-195}, keywords = {Reasoning, Description Logics, Optimisations, Optimizations}, tags = {AutomatedReasoning}, web_url = {http://link.springer.com/chapter/10.1007{\%}2F978-3-319-11915-1\_12}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2014/GKLT14b.pdf} } @Inproceedings { Kaz:Kli:2013:Android:ORE, author = {Kazakov, Yevgeny and Klinov, Pavel}, title = {Experimenting with ELK Reasoner on Android}, abstract = {This paper presents results of a preliminary evaluation of the OWL EL reasoner ELK running on a Google Nexus 4 cell phone under Android 4.2 OS. The results show that economic and well-engineered ontology reasoners can demonstrate acceptable performance when classifying ontologies with thousands of axioms and take advantage of multi-core CPUs of modern mobile devices. The paper emphasizes the engineering aspects of ELK's design and implementation which make this performance possible.}, year = {2013}, booktitle = {ORE}, volume = {1015}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, pages = {68-74}, tags = {KnowledgeModeling, ELK, LiveOntologies}, web_url = {http://ceur-ws.org/Vol-1015/paper\_9.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2013/KazKli13Android\_ORE.pdf} } @Inproceedings { DBLP:conf/semweb/KazakovK13a, author = {Kazakov, Yevgeny and Klinov, Pavel}, title = {Incremental Reasoning in OWL EL without Bookkeeping.}, year = {2013}, booktitle = {The Semantic Web - ISWC 2013 - 12th International Semantic Web Conference, Sydney, NSW, Australia, October 21-25, 2013, Proceedings, Part I}, pages = {232--247}, file_url = {http://dx.doi.org/10.1007/978-3-642-41335-3\_15} } @Inproceedings { KazKli:13:Incremental:DL, author = {Kazakov, Yevgeny and Klinov, Pavel}, title = {Incremental Reasoning in EL+ without Bookkeeping}, abstract = {We describe a method for updating the classification of ontologies expressed in the EL family of Description Logics after some axioms have been added or deleted. While incremental classification modulo additions is relatively straightforward, handling deletions is more problematic since it requires retracting logical consequences that no longer hold. Known algorithms address this problem using various forms of bookkeeping to trace the consequences back to premises. But such additional data can consume memory and place an extra burden on the reasoner during application of inferences. In this paper, we present a technique, which avoids this extra cost while being still very efficient for small incremental changes in ontologies.}, year = {2013}, booktitle = {DL}, volume = {1014}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, pages = {294-315}, tags = {KnowledgeModeling, ELK, LiveOntologies}, web_url = {http://ceur-ws.org/Vol-1014/paper\_33.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2013/KazKli13Incremental\_DL.pdf} } @Inproceedings { KazKli:13:ELK:Incremental:ISWC, author = {Kazakov, Yevgeny and Klinov, Pavel}, title = {Incremental Reasoning in OWL EL without Bookkeeping}, abstract = {We describe a method for updating the classification of ontologies expressed in the EL family of Description Logics after some axioms have been added or deleted. While incremental classification modulo additions is relatively straightforward, handling deletions is more problematic since it requires retracting logical consequences that are no longer valid. Known algorithms address this problem using various forms of bookkeeping to trace the consequences back to premises. But such additional data can consume memory and place an extra burden on the reasoner during application of inferences. In this paper, we present a technique, which avoids this extra cost while being very efficient for small incremental changes in ontologies. The technique is freely available as a part of the open-source EL reasoner ELK and its efficiency is demonstrated on naturally occurring and synthetic data.}, year = {2013}, DOI = {10.1007/978-3-642-41335-3\_15}, booktitle = {ISWC}, volume = {8218}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {232-247}, tags = {KnowledgeModeling, ELK, LiveOntologies}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2013/KazKli13Incremental\_ISWC.pdf} } @Inproceedings { GKKS13a, author = {Glimm, Birte and Kazakov, Yevgeny and Kollia, Ilianna and Stamou, Giorgos}, title = {Using the TBox to Optimise SPARQL Queries}, abstract = {We present an approach for using schema knowledge from the TBox to optimize the evaluation of SPARQL queries. The queries are evaluated over an OWL ontology using the OWL Direct Semantics entailment regime. For conjunctive instance queries, we proceed by transforming the query into an ABox. We then show how the TBox and this (small) query ABox can be used to build a maximal equivalent query where the additional query atoms can be used for reducing the set of possible mappings for query variables. We also consider arbitrary SPARQL queries and show how the concept and role hierarchies can be used to prune the search space of possible answers based on the polarity of variable occurrences in the query. We provide a prototypical implementation and evaluate the efficiency of the proposed optimizations. Our experimental study shows that the use of the proposed optimizations leads to a significant improvement in the execution times of many queries.}, year = {2013}, booktitle = {Proceedings of the 2013 International Description Logic Workshop (DL 2013)}, publisher = {CEUR Workshop Proceedings}, keywords = {SPARQL, OWL, Description Logics, Query Answering, Optimisations, Optimizations}, tags = {AutomatedReasoning}, web_url = {http://ceur-ws.org/Vol-1014/paper\_80.pdf}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2013/GKKS13a.pdf} } @Inproceedings { KazKroSim12ELK_ORE, author = {Kazakov, Yevgeny and Kr\"{o}tzsch, Markus and Siman\v{c}\'{i}k, Franti\v{s}ek}, title = {ELK Reasoner: Architecture and Evaluation}, abstract = {ELK is a specialized reasoner for the lightweight ontology language OWL EL. The practical utility of ELK is in its combination of high performance and comprehensive support for language features. At its core, ELK employs a consequence-based reasoning engine that can take advantage of multi-core and multi-processor systems. A modular ar- chitecture allows ELK to be used as a stand-alone application, Prot\'{e}g\'{e} plug-in, or programming library (either with or without the OWL API). This system description presents the current state of ELK and experi- mental results with some difficult OWL EL ontologies.}, year = {2012}, booktitle = {Proceedings of the 1st International Workshop on OWL Reasoner Evaluation (\{ORE\} 2012)}, tags = {SemanticTechnologies, AutomatedReasoning, ELK}, web_url = {http://ceur-ws.org/Vol-858/ore2012\_paper10.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2012/KazKroSim12ELK\_ORE.pdf} } @Techreport { KazKroSim12ELK_TR, author = {Kazakov, Yevgeny and Kr\"{o}tzsch, Markus and Siman\v{c}\'{i}k, Franti\v{s}ek}, title = {ELK: A Reasoner for OWL EL Ontologies}, abstract = {ELK is a specialized reasoner for the lightweight ontology language OWL EL. The practical utility of ELK is in its combination of high performance and comprehensive support for language features. At its core, ELK employs a consequence-based reasoning engine that can take advantage of multi-core and multi-processor systems. A modular architecture allows ELK to be used as a stand-alone application, Prot\'{e}g\'{e} plug-in, or programming library (either with or without the OWL API). This system description presents the current state of ELK.}, year = {2012}, institution = {University of Oxford}, tags = {AutomatedReasoning, ELK}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2012/KazKroSim12ELK\_TR.pdf} } @Conference { KazKroSim12NominalsEL_KR, author = {Kazakov, Yevgeny and Kr\"{o}tzsch, Markus and Siman\v{c}\'{i}k, Franti\v{s}ek}, title = {Practical Reasoning with Nominals in the EL Family of Description Logics}, abstract = {The EL family of description logics (DLs) has been designed to provide a restricted syntax for commonly used DL constructors with the goal to guarantee polynomial complexity of reasoning. Yet, polynomial complexity does not always mean that the underlying reasoning procedure is efficient in practice. In this paper we consider a simple DL ELO from the EL family that admits nominals, and argue that existing polynomial reasoning procedures for ELO can be impractical for many realistic ontologies. To solve the problem, we describe an optimization strategy in which the inference rules required for reasoning with nominals are avoided as much as possible. The optimized procedure is evaluated within the reasoner ELK and demonstrated to perform well in practice.}, year = {2012}, isbn = {978-1-57735-560-1}, booktitle = {Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning (\{KR\} 2012)}, publisher = {AAAI Press}, editor = {Gerhard Brewka and Thomas Eiter and Sheila A. McIlraith}, tags = {KnowledgeModeling, ELK, LiveOntologies}, web_url = {http://www.aaai.org/ocs/index.php/KR/KR12/paper/view/4540}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2012/KazKroSim12NominalsEL\_KR.pdf} } @Inproceedings { KazKroSim:11:Unchain:DL, author = {Kazakov, Yevgeny and Kr\"{o}tzsch, Markus and Siman\v{c}\'{i}k, Franti\v{s}ek}, title = {Unchain My EL Reasoner}, abstract = {We study a restriction of the classification procedure for EL++ where the inference rule for complex role inclusion axioms (RIAs) is applied in a ``left-linear\\" way in analogy with the well-known procedure for computing the transitive closure of a binary relation. We introduce a notion of left-admissibility for a set of RIAs, which specifies when a subset of RIAs can be used in a left-linear way without loosing consequences, prove a criterion which can be used to effectively check this property, and describe somepreliminary experimental results analyzing when the restricted procedure can give practical improvements.}, year = {2011}, booktitle = {Description Logics}, volume = {745}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Riccardo Rosati and Sebastian Rudolph and Michael Zakharyaschev}, tags = {KnowledgeModeling}, web_url = {http://ceur-ws.org/Vol-745/paper\_54.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2011/KazKroSim11Unchain\_DL.pdf} } @Inproceedings { GliKazLut:11:QIO:DL, author = {Kazakov, Yevgeny and Lutz, Carsten and Glimm, Birte}, title = {Status QIO: An Update}, abstract = {We prove that conjunctive query answering in the description logic ALCOIF is co-N2ExpTime-hard, thus improving the previously known 2ExpTime lower bound. The result transfers to OWL DL and OWL2 DL, of which ALCOIF is an important fragment. A matching upper bound remains open.}, year = {2011}, booktitle = {Description Logics}, volume = {745}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Riccardo Rosati and Sebastian Rudolph and Michael Zakharyaschev}, tags = {KnowledgeModeling}, web_url = {http://ceur-ws.org/Vol-745/paper\_44.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2011/GliKazLut11QIO\_DL.pdf} } @Inproceedings { KazKroSim:11:Concurrent:ISWC, author = {Kazakov, Yevgeny and Kr\"{o}tzsch, Markus and Siman\v{c}\'{i}k, Franti\v{s}ek}, title = {Concurrent Classification of EL Ontologies}, abstract = {We describe an optimised consequence-based procedure for classification of ontologies expressed in a polynomial fragment ELHR+ of the OWL 2 EL profile. A distinguishing property of our procedure is that it can take advantage of multiple processors/cores, which increasingly prevail in computer systems. Our solution is based on a variant of the ``given clause\\" saturation algorithm for first-order theorem proving, where we assign derived axioms to ``contexts\\" within which they can be used and which can be processed independently. We describe an implementation of our procedure within the Java-based reasoner ELK. Our implementation is light-weight in the sense that an overhead of managing concurrent computations is minimal. This is achieved by employing lock-free data structures and operations such as ``compare-and-swap\\". We report on preliminary experimental results demonstrating a substantial speedup of ontology classification on multi-core systems. In particular, one of the largest and widely-used medical ontologies SNOMED CT can be classified in as little as 5 seconds.}, year = {2011}, booktitle = {ISWC}, tags = {KnowledgeModeling, ELK}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2011/KazKroSim11Concurrent\_ISWC.pdf} } @Inproceedings { SimKazHor:11:BeyondHorn:IJCAI, author = {Siman\v{c}\'{i}k, Franti\v{s}ek and Kazakov, Yevgeny and Horrocks, Ian}, title = {Consequence-Based Reasoning beyond Horn Ontologies}, abstract = {Consequence-based ontology reasoning procedures have so far been known only for Horn ontology languages. A difficulty in extending such procedures is that non-Horn axioms seem to require reasoning by case, which causes non-determinism in tableau-based procedures. In this paper we present a consequence-based procedure for ALCH that overcomes this difficulty by using rules similar to ordered resolution to deal with disjunctive axioms in a deterministic way; it retains all the favourable attributes of existing consequence-based procedures, such as goal-directed 'one pass' classification, optimal worst-case complexity, and 'pay-as-you-go' behaviour. Our preliminary empirical evaluation suggests that the procedure scales well to non-Horn ontologies.}, year = {2011}, booktitle = {IJCAI}, pages = {1093-1099}, tags = {KnowledgeModeling}, web_url = {http://ijcai.org/papers11/Papers/IJCAI11-187.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2011/SimKazHor11BeyondHorn.pdf} } @Inproceedings { Kazakov:10:Regularity:IJCAR, author = {Kazakov, Yevgeny}, title = {An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ}, abstract = {We propose an extension of the syntactic restriction for complex role inclusion axioms in the description logic SROIQ. Like the original restriction in SROIQ, our restrictions can be checked in polynomial time and they guarantee regularity for the sets of role chains implying roles, and thereby decidability for the main reasoning problems. But unlike the original restrictions, our syntactic restrictions can represent any regular compositional properties on roles. In particular, many practically relevant complex role inclusion axioms, such as those describing various parthood relations, can be expressed in our extension, but could not be expressed in the original SROIQ.}, year = {2010}, booktitle = {IJCAR}, volume = {6173}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {472-486}, web_url = {10.1007/978-3-642-14203-1\_40}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2010/Kaz10Regularity.pdf} } @Article { CueHalKazSun:10:Incremental:JAR, author = {Cuenca Grau, Bernardo and Halaschek-Wiener, Christian and Kazakov, Yevgeny and Suntisrivaraporn, Boontawee}, title = {Incremental Classification of Description Logics Ontologies}, abstract = {The development of ontologies involves continuous but relatively small modifications. However, existing ontology reasoners do not take advantage of the similarities between different versions of an ontology. In this paper, we propose a collection of techniques for incremental reasoning -- that is, reasoning that reuses information obtained from previous versions of an ontology. We have applied our results to incremental classification of OWL ontologies and found significant improvement over regular classification time on a set of real-world ontologies.}, year = {2010}, journal = {JAR}, volume = {44}, pages = {337-369}, number = {4}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2010/CueHalKazSun10Incremental\_JAR.pdf} } @Inproceedings { MagKazHor:10:NDR:DL, author = {Magka, Despoina and Kazakov, Yevgeny and Horrocks, Ian}, title = {Tractable Extensions of the Description Logic EL with Numerical Datatypes}, year = {2010}, booktitle = {Description Logics}, volume = {573}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Volker Haarslev and David Toman and Grant Weddell}, web_url = {http://CEUR-WS.org/Vol-573/paper\_29.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2010/MagKazHor10NDR\_DL.pdf} } @Inproceedings { MagKazHor:10:NDR:IJCAR, author = {Magka, Despoina and Kazakov, Yevgeny and Horrocks, Ian}, title = {Tractable Extensions of the Description Logic EL with Numerical Datatypes}, abstract = {We consider extensions of the lightweight description logic (DL) EL with numerical datatypes such as naturals, integers, rationals and reals equipped with relations such as equality and inequalities. It is well-known that the main reasoning problems for such DLs are decidable in polynomial time provided that the datatypes enjoy the so-called convexity property. Unfortunately many combinations of the numerical relations violate convexity, which makes the usage of these datatypes rather limited in practice. In this paper, we make a more fine-grained complexity analysis of these DLs by considering restrictions not only on the kinds of relations that can be used in ontologies but also on their occurrences, such as allowing certain relations to appear only on the left-hand side of the axioms. To this end, we introduce a notion of safety for a numerical datatype with restrictions (NDR) which guarantees tractability, extend the EL reasoning algorithm to these cases, and provide a complete classification of safe NDRs for natural numbers, integers, rationals and reals.}, year = {2010}, booktitle = {IJCAR}, volume = {6173}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {61-75}, web_url = {10.1007/978-3-642-14203-1\_6}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2010/MagKazHor10NDR.pdf} } @Inproceedings { KazakovPrattHartman:09:Graded, author = {Kazakov, Yevgeny and Pratt-Hartmann, Ian}, title = {A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics}, abstract = {Graded modal logic is the formal language obtained from ordinary (propositional) modal logic by endowing its modal operators with cardinality constraints. Under the familiar possible-worlds semantics, these augmented modal operators receive interpretations such as \dqIt is true at no fewer than 15 accessible worlds that...\dq, or \dqIt is true at no more than 2 accessible worlds that...\dq. We investigate the complexity of satisfiability for this language over some familiar classes of frames. This problem is more challenging than its ordinary modal logic counterpart---especially in the case of transitive frames, where graded modal logic lacks the tree-model property. We obtain tight complexity bounds for the problem of determining the satisfiability of a given graded modal logic formula over the classes of frames characterized by any combination of reflexivity, seriality, symmetry, transitivity and the Euclidean property.}, year = {2009}, booktitle = {LICS}, publisher = {IEEE Computer Society}, pages = {407-416}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2009/KazPH09Graded.pdf} } @Inproceedings { Kazakov:09:Regularity:DL, author = {Kazakov, Yevgeny}, title = {An Extension of Regularity Conditions for Complex Role Inclusion Axioms}, year = {2009}, booktitle = {Description Logics}, volume = {477}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Bernardo Cuenca Grau and Ian Horrocks and Boris Motik and Ulrike Sattler}, web_url = {http://ceur-ws.org/Vol-477/paper\_68.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2009/Kaz09Regularity\_DL.pdf} } @Inproceedings { DelKaz:09:SQL:OWLED, author = {Delaitre, Vincent and Kazakov, Yevgeny}, title = {Classifying ELH Ontologies In SQL Databases}, abstract = {The current implementations of ontology classification procedures use the main memory of the computer for loading and processing ontologies, which soon can become one of the main limiting factors for very large ontologies. We describe a secondary memory implementation of a classification procedure for ELH ontologies using an SQL relational database management system. Although secondary memory has much slower characteristics, our preliminary experiments demonstrate that one can obtain a comparable performance to those of existing in-memory reasoners using a number of caching techniques.}, year = {2009}, booktitle = {OWL: Experiences and Directions 2009 (OWLED 2009)}, address = {Chantilly, VA, United States}, web_url = {http://CEUR-WS.org/Vol-529/owled2009\_submission\_44.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2009/DalKaz09SQL.pdf} } @Inproceedings { Kazakov:09:CB:DL, author = {Kazakov, Yevgeny}, title = {Consequence-Driven Reasoning for Horn SHIQ Ontologies}, year = {2009}, booktitle = {Description Logics}, volume = {477}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, editor = {Bernardo Cuenca Grau and Ian Horrocks and Boris Motik and Ulrike Sattler}, web_url = {http://ceur-ws.org/Vol-477/paper\_69.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2009/Kaz09CB\_DL.pdf} } @Incollection { GraHorKazSat:09:Modules:Book, author = {Cuenca Grau, Bernardo and Horrocks, Ian and Kazakov, Yevgeny and Sattler, Ulrike}, title = {Extracting Modules from Ontologies: A Logic-Based Approach}, abstract = {The ability to extract meaningful fragments from an ontology is essential for ontology reuse. We propose a definition of a module that guarantees to completely capture the meaning of a given set of terms, i.e., to include all axioms relevant to the meaning of these terms. We show that the problem of determining whether a subset of an ontology is a module for a given vocabulary is undecidable even for OWL DL. Given these negative results, we propose sufficient conditions for a for a fragment of an ontology to be a module. We propose an algorithm for computing modules based on those conditions and present our experimental results on a set of real-world ontologies of varying size and complexity.}, year = {2009}, isbn = {978-3-642-01906-7}, booktitle = {Modular Ontologies}, volume = {5445}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {159-186}, web_url = {10.1007/978-3-642-01907-4\_8} } @Inproceedings { GrauMotikKaz:09:Import, author = {Cuenca Grau, Bernardo and Motik, Boris and Kazakov, Yevgeny}, title = {Import-by-Query: Ontology Reasoning under Access Limitations}, abstract = {To enable ontology reuse, the Web Ontology Language (OWL) allows an ontology Kv to import an ontology Kh. To reason with such a Kv, a reasoner needs physical access to the axioms of Kh. For copyright and/or privacy reasons, however, the authors of Kh might not want to publish the axioms of Kh; instead, they might prefer to provide an oracle that can answer a (limited) set of queries over Kh, thus allowing Kv to import Kh \dqby query.\dq In this paper, we study import-by-query algorithms, which can answer questions about Kv U Kh by accessing only Kv and the oracle. We show that no such algorithm exists in general, and present restrictions under which importing by query becomes feasible.}, year = {2009}, booktitle = {IJCAI}, pages = {727-732}, file_url = {http://ijcai.org/papers09/Papers/IJCAI09-126.pdf} } @Inproceedings { Kazakov:08:RIQ:SROIQ, author = {Kazakov, Yevgeny}, title = {RIQ and SROIQ Are Harder than SHOIQ}, abstract = {We identify the computational complexity of (finite model) reasoning in the sublanguages of the description logic SROIQ---the logic currently proposed as the basis for the next version of the web ontology language OWL. We prove that the classical reasoning problems are N2ExpTime-complete for SROIQ and 2ExpTime-hard for its sub-language RIQ. RIQ and SROIQ are thus exponentially harder than SHIQ and SHOIQ. The growth in complexity is due to complex role inclusion axioms of the form R1 o ... o Rn [ R, which are known to cause an exponential blowup in the tableau-based procedures for RIQ and SROIQ. Our complexity results, thus, also prove that this blowup is unavoidable. We also demonstrate that the hardness results hold already for linear role inclusion axioms of theform R1 o R2 [ R1 and R1 o R2 [ R2.}, year = {2008}, booktitle = {KR}, publisher = {AAAI Press}, pages = {274-284}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2008/Kaz08SROIQ\_KR.pdf} } @Techreport { GlKa08bb, author = {Glimm, Birte and Kazakov, Yevgeny}, title = {Role Conjunctions in Expressive Description Logics}, abstract = {We show that adding role conjunctions to the prominent DLs SHIF and SHOIN causes a jump in the computational complexity of the standard reasoning tasks from ExpTime to 2ExpTime already for SHI and from NExpTime to N2ExpTime for SHOIF. We further show that this increase in complexity is due to a subtle interaction between inverse roles, role hierarchies, and role transitivity in the presence of role conjunctions and that for the DL SHQ a jump in the computational complexity cannot be observed.}, year = {2008}, DOI = {10.1007/978-3-540-89439-1\_28}, institution = {The University of Oxford}, booktitle = {Proceedings of the 15th International Conference on Logic for Programming and Automated Reasoning (LPAR 2008)}, volume = {5330}, publisher = {Lecture Notes in Computer Science}, pages = {391-405}, web_url = {http://www.springerlink.com/content/r5641x1502220vv2/}, file_url = {https://www.uni-ulm.de/fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2008/GlKa08b.pdf} } @Article { CueHorKazSat:08:Modularity, author = {Cuenca Grau, Bernardo and Horrocks, Ian and Kazakov, Yevgeny and Sattler, Ulrike}, title = {Modular Reuse of Ontologies: Theory and Practice}, abstract = {In this paper, we propose a set of tasks that are relevant for the modular reuse of ontologies. In order to formalize these tasks as reasoning problems, we introduce the notions of conservative extension, safety and module for a very general class of logic-based ontology languages. We investigate the general properties of and relationships between these notions and study the relationships between the relevant reasoning problems we have previously identified. To study the computability of these problems, we consider, in particular, Description Logics (DLs), which provide the formal underpinning of the W3C Web Ontology Language (OWL), and show that all the problems we consider are undecidable or algorithmically unsolvable for the description logic underlying OWL DL. In order to achieve a practical solution, we identify conditions sufficient for an ontology to reuse a set of symbols ``safely\\"---that is, without changing their meaning. We provide the notion of a safety class, which characterizes any sufficient condition for safety, and identify a family of safety classes--called locality---which enjoys a collection of desirable properties. We use the notion of a safety class to extract modules from ontologies, and we provide various modularization algorithms that are appropriate to the properties of the particular safety class in use. Finally, we show practical benefits of our safety checking and module extraction algorithms.}, year = {2008}, journal = {JAIR}, volume = {31}, pages = {273-318}, web_url = {http://www.jair.org/papers/paper2375.html}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2008/CueHorKazSat08Modularity\_JAIR.pdf} } @Article { KazMot:08:SHOIQ:JAR, author = {Kazakov, Yevgeny and Motik, Boris}, title = {A Resolution-Based Decision Procedure for SHOIQ}, abstract = {We present a resolution-based decision procedure for the description logic SHOIQ-the logic underlying the Semantic Web ontology language OWL-DL. Our procedure is goal-oriented, and it naturally extends a similar procedure for SHIQ, which has proven itself in practice. Extending this procedure to SHOIQ using existing techniques is not straightforward because of nominals, number restrictions, and inverse roles-a combination known to cause termination problems. We overcome this difficulty by using basic superposition calculus extended with custom simplification rules.}, year = {2008}, journal = {JAR}, volume = {40}, pages = {89-116}, number = {2-3}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2008/KazMot08SHOIQ\_JAR.pdf} } @Inproceedings { CueHorKazSat:07:Framework, author = {Cuenca Grau, Bernardo and Horrocks, Ian and Kazakov, Yevgeny and Sattler, Ulrike}, title = {A Logical Framework for Modularity of Ontologies.}, abstract = {Modularity is a key requirement for collaborative ontology engineering and for distributed ontology reuse on the Web. Modern ontology languages, such as OWL, are logic-based, and thus a useful notion of modularity needs to take the semantics of ontologies and their implications into account. We propose a logic-based notion of modularity that allows the modeler to specify the external signature of their ontology, whose symbols are assumed to be defined in some other ontology. We define two restrictions on the usage of the external signature, a syntactic and a slightly less restrictive, semantic one, each of which is decidable and guarantees a certain kind of \dqblack-box\dq behavior, which enables the controlled merging of ontologies. Analysis of real-world ontologies suggests that these restrictions are not too onerous.}, year = {2007}, booktitle = {IJCAI}, pages = {298-303}, web_url = {http://www.ijcai.org/papers07/Papers/IJCAI07-046.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2007/CueHorKazSat07Framework.pdf} } @Inproceedings { CueHalKaz:07:Incremental, author = {Cuenca Grau, Bernardo and Halaschek-Wiener, Christian and Kazakov, Yevgeny}, title = {History Matters: Incremental Ontology Reasoning Using Modules}, abstract = {The development of ontologies involves continuous but relatively small modifications. Existing ontology reasoners, however, do not take advantage of the similarities between different versions of an ontology. In this paper, we propose a technique for incremental reasoning---that is, reasoning that reuses information obtained from previous versions of an ontology---based on the notion of a module. Our technique does not depend on a particular reasoning calculus and thus can be used in combination with any reasoner. We have applied our results to incremental classification of OWL DL ontologies and found significant improvement over regular classification time on a set of real-world ontologies.}, year = {2007}, booktitle = {ISWC/ASWC}, volume = {4825}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {183-196}, web_url = {10.1007/978-3-540-76298-0\_14}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2007/CueHalKaz07Incremental.pdf} } @Inproceedings { KazSatZol:07:NonSimple, author = {Kazakov, Yevgeny and Sattler, Ulrike and Zolin, Evgeny}, title = {How Many Legs Do I Have? Non-Simple Roles in Number Restrictions Revisited}, abstract = {The Description Logics underpinning OWL impose a well-known syntactic restriction in order to preserve decidability: they do not allow to use non-simple roles-that is, transitive roles or their super-roles-in number restrictions. When modeling composite objects, for example in bio-medical ontologies, this restriction can pose problems. Therefore, we take a closer look at the problem of counting over non-simple roles. On the one hand, we sharpen the known undecidability results and demonstrate that: (i) for DLs with inverse roles, counting over non-simple roles leads to undecidability even when there is only one role in the language; (ii) for DLs without inverses, two transitive and an arbitrary role are sufficient for undecidability. On the other hand, we demonstrate that counting over non-simple roles does not compromise decidability in the absence of inverse roles provided that certain restrictions on role inclusion axioms are satisfied}, year = {2007}, booktitle = {LPAR}, volume = {4790}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {303-317}, web_url = {10.1007/978-3-540-75560-9\_23}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2007/KazSatZol07Legs.pdf} } @Techreport { KazSatZol:07:RBox, author = {Kazakov, Yevgeny and Sattler, Ulrike and Zolin, Evgeny}, title = {Is Your RBox Safe?}, abstract = {The Description Logics underpinning OWL impose a well-known syntactic restriction in order to preserve decidability: they do not allow to use non-simple roles---that is, transitive roles or their super-roles---in number restrictions. When modeling composite objects, for example in bio-medical ontologies, this restriction can pose problems. Therefore, we take a closer look at the problem of counting over non-simple roles. On the one hand, we sharpen the known undecidability results and demonstrate that: (i) for DLs with inverse roles, counting over non-simple roles leads to undecidability even when there is only one role in the language; (ii) for DLs without inverses, two transitive and an arbitrary role are sufficient for undecidability. On the other hand, we demonstrate that counting over non-simple roles does not compromise decidability in the absence of inverse roles provided that certain restrictions on role inclusion axioms are satisfied.}, type = {Research Report}, year = {2007}, institution = {The University of Manchester}, address = {Oxford Road, Manchester M13 9PL, UK}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2007/KazSatZol07RBox\_TR.pdf} } @Inproceedings { CueHorKazSat:07:Modules, author = {Cuenca Grau, Bernardo and Horrocks, Ian and Kazakov, Yevgeny and Sattler, Ulrike}, title = {Just the Right Amount: Extracting Modules from Ontologies.}, abstract = {The ability to extract meaningful fragments from an ontology is essential for ontology re-use. We propose a definition of a module that guarantees to completely capture the meaning of a given set of terms, i.e., to include all axioms relevant to the meaning of these terms, and study the problem of extracting minimally sized modules. We show that the problem of determining whether a subset of an ontology is a module for a given vocabulary is undecidable even for rather restricted sub-languages of OWL DL. Hence we propose two \dqapproximations\dq, i.e., alternative definitions of modules for a vocabulary that still provide the above guarantee, but that are possibly too strict, and that may thus result in larger modules: the first approximation is semantic and can be checked using existing DL reasoners; the second is syntactic, and can be computed in polynomial time. Finally, we report on an empirical evaluation of our syntactic approximation that demonstrates that the modules we extract are surprisingly small.}, year = {2007}, booktitle = {WWW}, publisher = {ACM}, address = {Banff, Canada}, pages = {717--726}, web_url = {http://www2007.org/proceedings.html}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2007/CueHorKazSat07Modularity.pdf} } @Inproceedings { CueHorKazSat:07:Safe, author = {Cuenca Grau, Bernardo and Horrocks, Ian and Kazakov, Yevgeny and Sattler, Ulrike}, title = {Ontology Reuse: Better Safe than Sorry.}, year = {2007}, booktitle = {Description Logics}, publisher = {Bozen/Bolzano University Press}, address = {Brixen/Bressanone, Italy}, pages = {41--52}, web_url = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-250/}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2007/CueHorKazSat07Safe.pdf} } @Phdthesis { Kazakov:06:Phd, author = {Kazakov, Yevgeny}, title = {Saturation-Based Decision Procedures for Extensions of the Guarded Fragment}, abstract = {We apply the framework of Bachmair and Ganzinger for saturation-based theorem proving to derive a range of decision procedures for logical formalisms, starting with a simple terminological language EL, which allows for conjunction and existential restrictions only, and ending with extensions of the guarded fragment with equality, constants, functionality, number restrictions and compositional axioms of form SoT=\\>H. Our procedures are derived in a uniform way using standard saturation-based calculi enhanced with simplification rules based on the general notion of redundancy. We argue that such decision procedures can be applied for reasoning in description logics, where they have certain advantages over traditionally used tableau procedures, such as optimal worst-case complexity and direct correctness proofs}, year = {2006}, school = {Universit\"{a}t des Saarlandes}, address = {Saarbr\"{u}cken, Germany}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2006/Kazakov06Phd.pdf} } @Unpublished { Kazakov:05:Framework, author = {Kazakov, Yevgeny}, title = {A Framework of Refutational Theorem Proving for Saturation-Based Decision Procedures}, abstract = {Automated state-of-the-art theorem provers are typically optimised for particular strategies, and there are only limited number of options that can be set by the user. Probably because of this, the general conditions on applicability of saturation-based calculi have not been thoroughly investigated. However for some applications, e.g., for saturation-based decision procedures, one would like to have more options in order to design flexible saturation strategies.In this report we revisit several well-known saturation-based calculi used in automated deduction: Ordered Resolution, Ordered Paramodulation, Superposition and Chaining calculi. We give a uniform account on completeness proofs for these calculi using the standard model construction procedures of Bachmair and Ganzinger. By careful inspection of these proofs, we formulate some variations of inference rules and general conditions on orderings under which the calculi remain refutationally complete. In particular, we considerably generalise the known class of admissible orderings for the Chaining calculi.We also consider in details the standard notion of redundancy, estimate the complexity for the steps of the clause normal form transformation, andgive a computational model of the saturation process.}, type = {Research Report}, year = {2005}, institution = {Max-Planck-Institut f\"{u}r Informatik}, address = {Stuhlsatzenhausweg 85, 66123 Saarbr\"{u}cken, Germany}, number = {MPI-I-2005-2-004}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2005/Kaz05Framework.pdf}, note = {Research Report MPI-I-2005-2-004, Max-Planck-Institut f\"{u}r Informatik, on revison} } @Inproceedings { Kazakov:04:GF2N, author = {Kazakov, Yevgeny}, title = {A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment.}, abstract = {We consider a two-variable guarded fragment with number restrictions for binary relations and give a satisfiability preserving transformation of formulas in this fragment to the three-variable guarded fragment. The translation can be computed in polynomial time and produces a formula that is linear in the size of the initial formula even for the binary coding of number restrictions. This allows one to reduce reasoning problems for many description logics to the satisfiability problem for the guarded fragment}, year = {2004}, booktitle = {JELIA}, volume = {3229}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {372-384}, web_url = {http://springerlink.metapress.com/openurl.asp?genre=article\\&issn=0302-9743\\&volume=3229\\&spage=372}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2004/Kaz04GF2N.pdf} } @Inproceedings { KazNiv:04:ResGFTG, author = {Kazakov, Yevgeny and de Nivelle, Hans}, title = {A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.}, abstract = {We show how well-known refinements of ordered resolution, in particular redundancy elimination and ordering constraints in combination with a selection function, can be used to obtain a decision procedure for the guarded fragment with transitive guards. Another contribution of the paper is a special scheme notation, that allows to describe saturation strategies and show their correctness in a concise form}, year = {2004}, booktitle = {IJCAR}, volume = {3097}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {122-136}, web_url = {http://springerlink.metapress.com/openurl.asp?genre=article\\&issn=0302-9743\\&volume=3097\\&spage=122}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2004/KazNiv04Res4GFTG.pdf} } @Unpublished { Kazakov:04:CombRes, author = {Kazakov, Yevgeny}, title = {Combining Resolution Decision Procedures}, abstract = {We present resolution-based decision procedures for the guarded, two-variable and monadic fragments without equality in a uniform way and show how they can be combined. In this way, new decidable fragments are obtained. We make use of a novel technique for describing resolution decision procedures by means of clause schemes. The scheme notation provides a convenient way of specifying decision procedures, proving their correctness and analyzing complexity of associated decision problems. We also show that many decidability results obtained in the paper cannot be extended to the case with equality}, year = {2004}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2004/Kaz04CombRes.pdf}, note = {unpublished manuscript, available from \urlhttp://web.comlab.ox.ac.uk/oucl/work/yevgeny.kazakov/publications/} } @Techreport { KazNiv:04:ResGFTG:TR, author = {Kazakov, Yevgeny and de Nivelle, Hans}, title = {Resolution Decision Procedures for the Guarded Fragment with Transitive Guards}, abstract = {We show how well-known refinements of ordered resolution, in particular redundancy elimination and ordering constraints in combination with a selection function, can be used to obtain a decision procedure for the guarded fragment with transitive guards. Another contribution of the paper is a special scheme notation, that allows to describe saturation strategies and show their correctness in a concise form}, type = {Research Report}, year = {2004}, issn = {0946-011X}, institution = {Max-Planck-Institut f\"{u}r Informatik}, address = {Stuhlsatzenhausweg 85, 66123 Saarbr\"{u}cken, Germany}, number = {MPI-I-2004-2-001}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2004/KazNiv04GFTG\_Tech.pdf} } @Techreport { KazNiv:03:SubsumptionFLzero:TR, author = {Kazakov, Yevgeny and de Nivelle, Hans}, title = {Subsumption of concepts in DL FL for (cyclic) terminologies with respect to descriptive semantics is PSPACE-complete}, abstract = {We prove the PSPACE-completeness of the subsumption problem for (cyclic) terminologies with respect to descriptive semantics in a simple Description Logic FL0, which allows for conjunctions and universal value restrictions only, thus solving the problem which was open for more than ten years}, type = {Research Report}, year = {2003}, issn = {0946-011X}, institution = {Max-Planck-Institut f\"{u}r Informatik}, address = {Stuhlsatzenhausweg 85, 66123 Saarbr\"{u}cken, Germany}, number = {MPI-I-2003-2-003}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2003/SubDL.pdf} } @Inproceedings { Kazakov:03:SubsumptionFLzero, author = {Kazakov, Yevgeny and de Nivelle, Hans}, title = {Subsumption of Concepts in FL0 for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACE-complete.}, abstract = {We close the gap in the complexity classification of subsumption in the simple description logic FL0, which allows for conjunctions and universal value restriction only. We prove that the subsumption problem in FL0 is PSPACE-complete for descriptive semantics when cyclic definitions are allowed. Our proof uses automata theory and as a by-product we establish the PSPACE-completeness of a certain decision problem for regular languages}, year = {2003}, booktitle = {Description Logics}, volume = {81}, series = {CEUR Workshop Proceedings}, web_url = {http://SunSITE.Informatik.RWTH-Aachen.de/Publications/CEUR-WS/Vol-81/kazakov.pdf}, file_url = {fileadmin/website\_uni\_ulm/iui.inst.090/Publikationen/2003/KazNiv03FL0.pdf} }