This file was created by the TYPO3 extension publications --- Timezone: CEST Creation date: 2025-05-01 Creation time: 23:49:08 --- Number of references 60 inproceedings GlKW22 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. 2022 Proceedings of the 35th International Workshop on Description Logics (DL 2022) 3263 CEUR-WS.org CEUR Workshop Proceedings Ofer Arieli and Martin Homola and Jean Christoph Jung and Marie-Laure Mugnier https://ceur-ws.org/Vol-3263/paper-11.pdf Birte Glimm Yevgeny Kazakov Michael Welt inproceedings GlKa22 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. 2022 Proceedings of the 35th International Workshop on Description Logics (DL 2022) 3263 CEUR-WS.org CEUR Workshop Proceedings Ofer Arieli and Martin Homola and Jean Christoph Jung and Marie-Laure Mugnier https://ceur-ws.org/Vol-3263/paper-10.pdf Birte Glimm Yevgeny Kazakov inproceedings DBLP:conf/rweb/GlimmK19 2019 10.1007/978-3-030-31423-1_1 Reasoning Web. Explainable Artificial Intelligence - 15th International Summer School 11810 Springer Lecture Notes in Computer Science Markus ����ö�ٳ������� and Daria Stepanova 1-64 KnowledgeModeling https://doi.org/10.1007/978-3-030-31423-1\_1 t3://file?uid=420338 Birte Glimm Yevgeny Kazakov conference KazSko:IJCAR18:Justifications 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. 2018 978-3-319-94204-9 10.1007/978-3-319-94205-6 IJCAR 10900 Springer Lecture Notes in Computer Science Didier Galmiche and Stephan Schulz and Roberto Sebastiani 609--626 KnowledgeModeling LiveOntologies https://doi.org/10.1007/978-3-319-94205-6_40 /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2018/KazSko18Justifications_IJCAR.pdf Yevgeny Kazakov Peter Skocovsky inproceedings KazSko:DL17:Justifications 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. 2017 Proceedings of the 30th International Workshop on Description Logics (DL 2017) 1879 CEUR-WS.org CEUR Workshop Proceedings Alessandro Artale and Birte Glimm and Roman Kontchakov KnowledgeModeling, LiveOntologies http://ceur-ws.org/Vol-1879/paper38.pdf /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2017/KazSko17Justifications_DL.pdf Yevgeny Kazakov Peter Skocovsky inproceedings KazPon:DL17:Integration 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. 2017 Proceedings of the 30th International Workshop on Description Logics (DL 2017) 1879 CEUR-WS.org CEUR Workshop Proceedings Alessandro Artale and Birte Glimm and Roman Kontchakov KnowledgeModeling, LiveOntologies http://ceur-ws.org/Vol-1879/paper59.pdf /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2017/KazPon17Integration_DL.pdf Yevgeny Kazakov Denis Ponomaryov conference GliKazTra:17:Abstraction:Horn:SHOIF:AAAI 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. 2017 Proceedings of the 31st AAAI Conference on Artificial Intelligence AAAI Press Satinder P. Singh and Shaul Markovitch 1114--1120 31st AAAI Conference on Artificial Intelligence San Francisco, California, USA AutomatedReasoning http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14726 /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2017/GlKT17a.pdf Birte Glimm Yevgeny Kazakov Trung-Kien Tran inproceedings GlKT17b 2017 Proceedings of the 30th International Workshop on Description Logics (DL 2017) 1879 CEUR-WS.org CEUR Workshop Proceedings AutomatedReasoning http://ceur-ws.org/Vol-1879/paper57.pdf /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2017/GlKT17b.pdf Birte Glimm Yevgeny Kazakov Trung-Kien Tran inproceedings KazKliStu:DL17:Explanations 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 ‘explanation 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. 2017 Proceedings of the 30th International Workshop on Description Logics (DL 2017) 1879 CEUR-WS.org CEUR Workshop Proceedings Alessandro Artale and Birte Glimm and Roman Kontchakov KnowledgeModeling, ELK, LiveOntologies http://ceur-ws.org/Vol-1879/paper31.pdf /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2017/KazKliStu17Explanations_DL.pdf Yevgeny Kazakov Pavel Klinov Alexander Stupnikov inproceedings GlKT16a 2016 Proceedings of the 29th International Workshop on Description Logics (DL 2016) 1577 CEUR-WS.org CEUR Workshop Proceedings AutomatedReasoning http://ceur-ws.org/Vol-1577/invited_paper_1.pdf /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2016/GlKT16a.pdf Birte Glimm Yevgeny Kazakov Trung-Kien Tran inproceedings GlKT16b 2016 Proceedings of the 10th International Conference on Web Reasoning and Rule Systems (RR 2016) 9898 Springer-Verlag Lecture Notes in Computer Science Magdalena Ortiz and Stefan Schlobach 77--93 Reasoning, Description Logics, Optimisations, Optimizations, Materialization, Materialisation, Abstraction AutomatedReasoning http://dx.doi.org/10.1007/978-3-319-45276-0_7 /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2016/GlKT16b.pdf Best Student Paper Award Birte Glimm Yevgeny Kazakov Trung-Kien Tran inproceedings KazKli:2015:Advancing-ELK:DL 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. 2015 DL 1350 CEUR-WS.org CEUR Workshop Proceedings Diego Calvanese and Boris Konev KnowledgeModeling, ELK, LiveOntologies http://ceur-ws.org/Vol-1350/paper-27.pdf /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2015/KazKli15Advancing-ELK_DL.pdf Yevgeny Kazakov Pavel Klinov inproceedings GKKS15b 2015 Proceedings of the 28th International Workshop on Description Logics (DL 2015) CEUR Workshop Proceedings Description Logics, Query Answering, Semantic Web, SPARQL AutomatedReasoning /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2015/GKKS15a.pdf Birte Glimm Yevgeny Kazakov Ilianna Kollia Giorgos Stamou inproceedings GKKS14a 2015 Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI 2015) AAAI Press Description Logics, Query Answering, Semantic Web, SPARQL AutomatedReasoning /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2015/GKKS15a.pdf Birte Glimm Yevgeny Kazakov Ilianna Kollia Giorgos Stamou inproceedings GKLT14b 2014 10.1007/978-3-319-11915-1_12 Proceedings of the 13th International Semantic Web Conference (ISWC 2014) 8797 Springer-Verlag Lecture Notes in Computer Science 180-195 Reasoning, Description Logics, Optimisations, Optimizations AutomatedReasoning http://link.springer.com/chapter/10.1007%2F978-3-319-11915-1_12 /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2014/GKLT14b.pdf Birte Glimm Yevgeny Kazakov Thorsten Liebig Trung-Kien Tran Vincent Vialard inproceedings GKLT14a 2014 Proceedings of the 27th International Workshop on Description Logics (DL 2014) 1193 CEUR-WS.org CEUR Workshop Proceedings 180-195 Reasoning, Description Logics, Optimisations, Optimizations AutomatedReasoning http://ceur-ws.org/Vol-1193/paper_6.pdf /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2014/GKLT14a.pdf Birte Glimm Yevgeny Kazakov Thorsten Liebig Trung-Kien Tran Vincent Vialard inproceedings KazKli:2014:Tableau-CB:DL 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. 2014 DL 1193 CEUR-WS.org CEUR Workshop Proceedings Meghyn Bienvenu and Magdalena Ortiz and Riccardo Rosati and Mantas Simkus 579-590 KnowledgeModeling, ELK, LiveOntologies http://ceur-ws.org/Vol-1193/paper_10.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2015/KazKli15Advancing-ELK_DL.pdf Yevgeny Kazakov Pavel Klinov inproceedings KazKli:14:ELK:Tracing:ISWC 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. 2014 ISWC 8797 Springer Lecture Notes in Computer Science 196--211 KnowledgeModeling, ELK, LiveOntologies fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2014/KazKli14Tracing_ISWC.pdf Yevgeny Kazakov Pavel Klinov inproceedings Kaz:Kli:2014:Tracing:DL 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. 2014 DL 1193 CEUR-WS.org CEUR Workshop Proceedings Meghyn Bienvenu and Magdalena Ortiz and Riccardo Rosati and Mantas Simkus 221-232 KnowledgeModeling, ELK, LiveOntologies http://ceur-ws.org/Vol-1193/paper_26.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2014/KazKli14Tracing_DL.pdf Yevgeny Kazakov Pavel Klinov article KazKroSim:14:ELK:JAR 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. 2014 10.1007/s10817-013-9296-3 JAR 53 1-61 1 KnowledgeModeling, ELK, LiveOntologies /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2014/KazKroSim13ELK_JAR.pdf Yevgeny Kazakov Markus ����ö�ٳ������� ������Գپ�š��� ����������čí�� inproceedings Kaz:Kli:2013:Android:ORE 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. 2013 ORE 1015 CEUR-WS.org CEUR Workshop Proceedings 68-74 KnowledgeModeling, ELK, LiveOntologies http://ceur-ws.org/Vol-1015/paper_9.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2013/KazKli13Android_ORE.pdf Yevgeny Kazakov Pavel Klinov inproceedings DBLP:conf/semweb/KazakovK13a 2013 The Semantic Web - ISWC 2013 - 12th International Semantic Web Conference, Sydney, NSW, Australia, October 21-25, 2013, Proceedings, Part I 232--247 http://dx.doi.org/10.1007/978-3-642-41335-3_15 Yevgeny Kazakov Pavel Klinov inproceedings KazKli:13:Incremental:DL 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. 2013 DL 1014 CEUR-WS.org CEUR Workshop Proceedings 294-315 KnowledgeModeling, ELK, LiveOntologies http://ceur-ws.org/Vol-1014/paper_33.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2013/KazKli13Incremental_DL.pdf Yevgeny Kazakov Pavel Klinov inproceedings KazKli:13:ELK:Incremental:ISWC 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. 2013 10.1007/978-3-642-41335-3_15 ISWC 8218 Springer Lecture Notes in Computer Science 232-247 KnowledgeModeling, ELK, LiveOntologies fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2013/KazKli13Incremental_ISWC.pdf Yevgeny Kazakov Pavel Klinov inproceedings GKKS13a 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. 2013 Proceedings of the 2013 International Description Logic Workshop (DL 2013) CEUR Workshop Proceedings SPARQL, OWL, Description Logics, Query Answering, Optimisations, Optimizations AutomatedReasoning http://ceur-ws.org/Vol-1014/paper_80.pdf /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2013/GKKS13a.pdf Birte Glimm Yevgeny Kazakov Ilianna Kollia Giorgos Stamou inproceedings KazKroSim12ELK_ORE 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égé 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. 2012 Proceedings of the 1st International Workshop on OWL Reasoner Evaluation ({ORE} 2012) SemanticTechnologies, AutomatedReasoning, ELK http://ceur-ws.org/Vol-858/ore2012_paper10.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2012/KazKroSim12ELK_ORE.pdf Yevgeny Kazakov Markus ����ö�ٳ������� ������Գپ�š��� ����������čí�� techreport KazKroSim12ELK_TR 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égé plug-in, or programming library (either with or without the OWL API). This system description presents the current state of ELK. 2012 University of Oxford AutomatedReasoning, ELK fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2012/KazKroSim12ELK_TR.pdf Yevgeny Kazakov Markus ����ö�ٳ������� ������Գپ�š��� ����������čí�� conference KazKroSim12NominalsEL_KR 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. 2012 978-1-57735-560-1 Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning ({KR} 2012) AAAI Press Gerhard Brewka and Thomas Eiter and Sheila A. McIlraith KnowledgeModeling, ELK, LiveOntologies http://www.aaai.org/ocs/index.php/KR/KR12/paper/view/4540 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2012/KazKroSim12NominalsEL_KR.pdf Yevgeny Kazakov Markus ����ö�ٳ������� ������Գپ�š��� ����������čí�� inproceedings KazKroSim:11:Concurrent:ISWC 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. 2011 ISWC KnowledgeModeling, ELK fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2011/KazKroSim11Concurrent_ISWC.pdf Yevgeny Kazakov Markus ����ö�ٳ������� ������Գپ�š��� ����������čí�� inproceedings SimKazHor:11:BeyondHorn:IJCAI 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. 2011 IJCAI 1093-1099 KnowledgeModeling http://ijcai.org/papers11/Papers/IJCAI11-187.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2011/SimKazHor11BeyondHorn.pdf ������Գپ�š��� ����������čí�� Yevgeny Kazakov Ian Horrocks inproceedings GliKazLut:11:QIO:DL 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. 2011 Description Logics 745 CEUR-WS.org CEUR Workshop Proceedings Riccardo Rosati and Sebastian Rudolph and Michael Zakharyaschev KnowledgeModeling http://ceur-ws.org/Vol-745/paper_44.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2011/GliKazLut11QIO_DL.pdf Yevgeny Kazakov Carsten Lutz Birte Glimm inproceedings KazKroSim:11:Unchain:DL 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. 2011 Description Logics 745 CEUR-WS.org CEUR Workshop Proceedings Riccardo Rosati and Sebastian Rudolph and Michael Zakharyaschev KnowledgeModeling http://ceur-ws.org/Vol-745/paper_54.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2011/KazKroSim11Unchain_DL.pdf Yevgeny Kazakov Markus ����ö�ٳ������� ������Գپ�š��� ����������čí�� inproceedings Kazakov:10:Regularity:IJCAR 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. 2010 IJCAR 6173 Springer Lecture Notes in Computer Science 472-486 10.1007/978-3-642-14203-1_40 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2010/Kaz10Regularity.pdf Yevgeny Kazakov article CueHalKazSun:10:Incremental:JAR 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. 2010 JAR 44 337-369 4 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2010/CueHalKazSun10Incremental_JAR.pdf Bernardo Cuenca Grau Christian Halaschek-Wiener Yevgeny Kazakov Boontawee Suntisrivaraporn inproceedings MagKazHor:10:NDR:IJCAR 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. 2010 IJCAR 6173 Springer Lecture Notes in Computer Science 61-75 10.1007/978-3-642-14203-1_6 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2010/MagKazHor10NDR.pdf Despoina Magka Yevgeny Kazakov Ian Horrocks inproceedings MagKazHor:10:NDR:DL 2010 Description Logics 573 CEUR-WS.org CEUR Workshop Proceedings Volker Haarslev and David Toman and Grant Weddell http://CEUR-WS.org/Vol-573/paper_29.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2010/MagKazHor10NDR_DL.pdf Despoina Magka Yevgeny Kazakov Ian Horrocks inproceedings KazakovPrattHartman:09:Graded 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 "It is true at no fewer than 15 accessible worlds that...", or "It is true at no more than 2 accessible worlds that...". 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. 2009 LICS IEEE Computer Society 407-416 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2009/KazPH09Graded.pdf Yevgeny Kazakov Ian Pratt-Hartmann inproceedings Kazakov:09:Regularity:DL 2009 Description Logics 477 CEUR-WS.org CEUR Workshop Proceedings Bernardo Cuenca Grau and Ian Horrocks and Boris Motik and Ulrike Sattler http://ceur-ws.org/Vol-477/paper_68.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2009/Kaz09Regularity_DL.pdf Yevgeny Kazakov inproceedings DelKaz:09:SQL:OWLED 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. 2009 OWL: Experiences and Directions 2009 (OWLED 2009)

Chantilly, VA, United States

http://CEUR-WS.org/Vol-529/owled2009_submission_44.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2009/DalKaz09SQL.pdf Vincent Delaitre Yevgeny Kazakov inproceedings Kazakov:09:CB:DL 2009 Description Logics 477 CEUR-WS.org CEUR Workshop Proceedings Bernardo Cuenca Grau and Ian Horrocks and Boris Motik and Ulrike Sattler http://ceur-ws.org/Vol-477/paper_69.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2009/Kaz09CB_DL.pdf Yevgeny Kazakov incollection GraHorKazSat:09:Modules:Book 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. 2009 978-3-642-01906-7 Modular Ontologies 5445 Springer Lecture Notes in Computer Science 159-186 10.1007/978-3-642-01907-4_8 Bernardo Cuenca Grau Ian Horrocks Yevgeny Kazakov Ulrike Sattler inproceedings GrauMotikKaz:09:Import 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 "by query." 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. 2009 IJCAI 727-732 http://ijcai.org/papers09/Papers/IJCAI09-126.pdf Bernardo Cuenca Grau Boris Motik Yevgeny Kazakov article KazMot:08:SHOIQ:JAR 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. 2008 JAR 40 89-116 2-3 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2008/KazMot08SHOIQ_JAR.pdf Yevgeny Kazakov Boris Motik article CueHorKazSat:08:Modularity 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. 2008 JAIR 31 273-318 http://www.jair.org/papers/paper2375.html fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2008/CueHorKazSat08Modularity_JAIR.pdf Bernardo Cuenca Grau Ian Horrocks Yevgeny Kazakov Ulrike Sattler inproceedings Kazakov:08:RIQ:SROIQ 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. 2008 KR AAAI Press 274-284 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2008/Kaz08SROIQ_KR.pdf Yevgeny Kazakov techreport GlKa08bb 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. 2008 10.1007/978-3-540-89439-1_28 The University of Oxford Proceedings of the 15th International Conference on Logic for Programming and Automated Reasoning (LPAR 2008) 5330 Lecture Notes in Computer Science 391-405 http://www.springerlink.com/content/r5641x1502220vv2/ /fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2008/GlKa08b.pdf Birte Glimm Yevgeny Kazakov inproceedings CueHorKazSat:07:Framework 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 "black-box" behavior, which enables the controlled merging of ontologies. Analysis of real-world ontologies suggests that these restrictions are not too onerous. 2007 IJCAI 298-303 http://www.ijcai.org/papers07/Papers/IJCAI07-046.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2007/CueHorKazSat07Framework.pdf Bernardo Cuenca Grau Ian Horrocks Yevgeny Kazakov Ulrike Sattler inproceedings CueHalKaz:07:Incremental 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. 2007 ISWC/ASWC 4825 Springer Lecture Notes in Computer Science 183-196 10.1007/978-3-540-76298-0_14 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2007/CueHalKaz07Incremental.pdf Bernardo Cuenca Grau Christian Halaschek-Wiener Yevgeny Kazakov inproceedings KazSatZol:07:NonSimple 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 2007 LPAR 4790 Springer Lecture Notes in Computer Science 303-317 10.1007/978-3-540-75560-9_23 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2007/KazSatZol07Legs.pdf Yevgeny Kazakov Ulrike Sattler Evgeny Zolin techreport KazSatZol:07:RBox 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. Research Report 2007 The University of Manchester

Oxford Road, Manchester M13 9PL, UK

fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2007/KazSatZol07RBox_TR.pdf Yevgeny Kazakov Ulrike Sattler Evgeny Zolin inproceedings CueHorKazSat:07:Modules 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 "approximations", 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. 2007 WWW ACM

Banff, Canada

717--726 http://www2007.org/proceedings.html fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2007/CueHorKazSat07Modularity.pdf Bernardo Cuenca Grau Ian Horrocks Yevgeny Kazakov Ulrike Sattler inproceedings CueHorKazSat:07:Safe 2007 Description Logics Bozen/Bolzano University Press

Brixen/Bressanone, Italy

41--52 http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-250/ fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2007/CueHorKazSat07Safe.pdf Bernardo Cuenca Grau Ian Horrocks Yevgeny Kazakov Ulrike Sattler phdthesis Kazakov:06:Phd 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 2006 Universität des Saarlandes

Saarbrücken, Germany

fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2006/Kazakov06Phd.pdf Yevgeny Kazakov unpublished Kazakov:05:Framework 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. Research Report 2005 Max-Planck-Institut für Informatik

Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany

MPI-I-2005-2-004 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2005/Kaz05Framework.pdf Research Report MPI-I-2005-2-004, Max-Planck-Institut für Informatik, on revison Yevgeny Kazakov inproceedings Kazakov:04:GF2N 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 2004 JELIA 3229 Springer Lecture Notes in Computer Science 372-384 http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3229&spage=372 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2004/Kaz04GF2N.pdf Yevgeny Kazakov inproceedings KazNiv:04:ResGFTG 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 2004 IJCAR 3097 Springer Lecture Notes in Computer Science 122-136 http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3097&spage=122 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2004/KazNiv04Res4GFTG.pdf Yevgeny Kazakov Hans de Nivelle unpublished Kazakov:04:CombRes 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 2004 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2004/Kaz04CombRes.pdf unpublished manuscript, available from \urlhttp://web.comlab.ox.ac.uk/oucl/work/yevgeny.kazakov/publications/ Yevgeny Kazakov techreport KazNiv:04:ResGFTG:TR 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 Research Report 2004 0946-011X Max-Planck-Institut für Informatik

Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany

MPI-I-2004-2-001 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2004/KazNiv04GFTG_Tech.pdf Yevgeny Kazakov Hans de Nivelle techreport KazNiv:03:SubsumptionFLzero:TR 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 Research Report 2003 0946-011X Max-Planck-Institut für Informatik

Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany

MPI-I-2003-2-003 fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2003/SubDL.pdf Yevgeny Kazakov Hans de Nivelle inproceedings Kazakov:03:SubsumptionFLzero 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 2003 Description Logics 81 CEUR Workshop Proceedings http://SunSITE.Informatik.RWTH-Aachen.de/Publications/CEUR-WS/Vol-81/kazakov.pdf fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2003/KazNiv03FL0.pdf Yevgeny Kazakov Hans de Nivelle