This file was created by the TYPO3 extension publications
--- Timezone: CEST
Creation date: 2020-08-07
Creation time: 20:58:56
--- Number of references
71
inproceedings
DBLP:conf/rweb/GlimmK19
Classical Algorithms for Reasoning and Explanation in Description
Logics
2019
10.1007/978-3-030-31423-1_1
Reasoning Web. Explainable Artificial Intelligence - 15th International
Summer School 2019, Bolzano, Italy, September 20-24, 2019, Tutorial
Lectures
11810
Springer
Lecture Notes in Computer Science
Markus Krötzsch 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
Enumerating Justifications using Resolution
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
Enumerating Justifications using Resolution
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
On the Complexity of Semantic Integration of OWL Ontologies
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 K.
Ponamaryov
conference
GliKazTra:17:Abstraction:Horn:SHOIF:AAAI
Ontology Materialization by Abstraction Refinement in Horn SHOIF
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
https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2017/GlKT17a.pdf
Birte
Glimm
Yevgeny
Kazakov
Trung-Kien
Tran
inproceedings
GlKT17b
Scalable Reasoning by Abstraction in DL-Lite
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
https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2017/GlKT17b.pdf
Birte
Glimm
Yevgeny
Kazakov
Trung-Kien
Tran
inproceedings
KazKliStu:DL17:Explanations
Towards Reusable Explanation Services in Protege
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
Ontology Materialization by Abstraction Refinement in Horn SHOIF
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
https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2016/GlKT16a.pdf
Birte
Glimm
Yevgeny
Kazakov
Trung-Kien
Tran
inproceedings
GlKT16b
Scalable Reasoning by Abstraction Beyond DL-Lite
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
https://www.uni-ulm.de/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
Advancing {ELK}: Not Only Performance Matters
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
Lower and Upper Bounds for SPARQL Queries over OWL Ontologies
2015
Proceedings of the 28th International Workshop on Description Logics (DL 2015)
CEUR Workshop Proceedings
Description Logics, Query Answering, Semantic Web, SPARQL
AutomatedReasoning
https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2015/GKKS15a.pdf
Birte
Glimm
Yevgeny
Kazakov
Ilianna
Kollia
Giorgos
Stamou
inproceedings
GKKS14a
Lower and Upper Bounds for SPARQL Queries over OWL Ontologies
2015
Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI 2015)
AAAI Press
Description Logics, Query Answering, Semantic Web, SPARQL
AutomatedReasoning
https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2015/GKKS15a.pdf
Birte
Glimm
Yevgeny
Kazakov
Ilianna
Kollia
Giorgos
Stamou
inproceedings
Kaz:Kli:2014:Tracing:DL
Goal-Directed Tracing of Inferences in {EL} Ontologies
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
inproceedings
KazKli:14:ELK:Tracing:ISWC
Goal-Directed Tracing of Inferences in {EL} Ontologies
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
article
KazKroSim:14:ELK:JAR
The Incredible {ELK}: From Polynomial Procedures to Efficient Reasoning with {EL} Ontologies
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
Krötzsch
František
Simančík
inproceedings
KazKli:2014:Tableau-CB:DL
Bridging the Gap between Tableau and Consequence-Based Reasoning
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
GKLT14b
Abstraction Refinement for Ontology Materialization
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
https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2014/GKLT14b.pdf
Birte
Glimm
Yevgeny
Kazakov
Thorsten
Liebig
Trung-Kien
Tran
Vincent
Vialard
inproceedings
GKLT14a
Abstraction Refinement for Ontology Materialization
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
https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2014/GKLT14a.pdf
Birte
Glimm
Yevgeny
Kazakov
Thorsten
Liebig
Trung-Kien
Tran
Vincent
Vialard
inproceedings
Kaz:Kli:2013:Android:ORE
Experimenting with {ELK} Reasoner on Android
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
KazKli:13:Incremental:DL
Incremental Reasoning in {EL+} without Bookkeeping
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
Incremental Reasoning in {OWL EL} without Bookkeeping
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
DBLP:conf/semweb/KazakovK13a
Incremental Reasoning in <prt>OWL</prt> <prt>EL</prt> without Bookkeeping.
2013
The Semantic Web - <prt>ISWC</prt> 2013 - 12th International Semantic Web Conference, Sydney, NSW, Australia, October 21-25, 2013, Proceedings, Part <prt>I</prt>
232--247
http://dx.doi.org/10.1007/978-3-642-41335-3_15
Yevgeny
Kazakov
Pavel
Klinov
inproceedings
GKKS13a
Using the TBox to Optimise SPARQL Queries
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
https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2013/GKKS13a.pdf
Birte
Glimm
Yevgeny
Kazakov
Ilianna
Kollia
Giorgos
Stamou
conference
KazKroSim12NominalsEL_KR
Practical Reasoning with Nominals in the {EL} Family of Description Logics
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
Krötzsch
František
Simančík
techreport
KazKroSim12ELK_TR
ELK: A Reasoner for OWL EL Ontologies
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
Krötzsch
František
Simančík
inproceedings
KazKroSim12ELK_ORE
{ELK} Reasoner: Architecture and Evaluation
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
Krötzsch
František
Simančík
inproceedings
KazKroSim:11:Concurrent:ISWC
Concurrent Classification of EL Ontologies
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
Krötzsch
František
Simančík
techreport
KazKroSim:11:Concurrent:TR
Concurrent Classification of EL Ontologies
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
Oxford University
KnowledgeModeling, ELK
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2011/KazKroSim11Concurrent_TR.pdf
Yevgeny
Kazakov
Markus
Krötzsch
František
Simančík
inproceedings
SimKazHor:11:BeyondHorn:IJCAI
Consequence-Based Reasoning beyond <prt>H</prt>orn Ontologies
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
František
Simančík
Yevgeny
Kazakov
Ian
Horrocks
techreport
SimKazHor:11:BeyondHorn:IJCAI:TR
Consequence-Based Reasoning beyond <prt>H</prt>orn Ontologies
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
Oxford University
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2011/SimKazHor11BeyondHorn_TR.pdf
František
Simančík
Yevgeny
Kazakov
Ian
Horrocks
inproceedings
GliKazLut:11:QIO:DL
Status <prt>QIO</prt>: An Update
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
Birte
Glimm
Yevgeny
Kazakov
Carsten
Lutz
article
MagKazHor:11:NDR:JAR
Tractable Extensions of the Description Logic <prt>EL</prt> with Numerical Datatypes.
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.
2011
JAR
KnowledgeModeling
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2011/MagKazHor11NDR_JAR.pdf
Despoina
Magka
Yevgeny
Kazakov
Ian
Horrocks
inproceedings
KazKroSim:11:Unchain:DL
Unchain My EL Reasoner
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
Krötzsch
František
Simančík
techreport
MagKazHor:10:NDR:TR
Tractable Extensions of the Description Logic <prt>EL</prt> with Numerical Datatypes.
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
Oxford University
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2010/MagKazHor10NDR_TR.pdf
Despoina
Magka
Yevgeny
Kazakov
Ian
Horrocks
inproceedings
MagKazHor:10:NDR:IJCAR
Tractable Extensions of the Description Logic <prt>EL</prt> with Numerical Datatypes.
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
Tractable Extensions of the Description Logic <prt>EL</prt> with Numerical Datatypes
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
article
CueHalKazSun:10:Incremental:JAR
Incremental Classification of Description Logics Ontologies
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
Kazakov:10:Regularity:IJCAR
An Extension of Complex Role Inclusion Axioms in the Description Logic <prt>SROIQ</prt>.
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
inproceedings
Kazakov:09:CB:DL
Consequence-Driven Reasoning for <prt>H</prt>orn <prt>SHIQ</prt> Ontologies
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
Extracting Modules from Ontologies: A Logic-Based Approach
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
Kazakov:09:CB
Consequence-Driven Reasoning for <prt>H</prt>orn <prt>SHIQ</prt> Ontologies
We present a novel reasoning procedure for Horn SHIQ ontologies-SHIQ ontologies that can be translated to the Horn fragment of first-order logic. In contrast to traditional reasoning procedures for ontologies, our procedure does not build models or model representations, but works by deriving new consequent axioms. The procedure is closely related to the so-called completion-based procedure for EL++ ontologies, and can be regarded as an extension thereof. In fact, our procedure is theoretically optimal for Horn SHIQ ontologies as well as for the common fragment of EL++ and SHIQ. A preliminary empirical evaluation of our procedure on large medical ontologies demonstrates a dramatic improvement over existing ontology reasoners. Specifically, our implementation allows the classification of the largest available OWL version of Galen. To the best of our knowledge no other reasoner is able to classify this ontology.
2009
IJCAI
2040-2045
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2009/Kaz09CB.pdf
Yevgeny
Kazakov
inproceedings
GrauMotikKaz:09:Import
Import-by-Query: Ontology Reasoning under Access Limitations
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
techreport
DelaitreKazakov:09:DB_TR
Classifying <prt>ELH</prt> Ontologies in <prt>SQL</prt> Databases
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
Oxford University
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2009/DelKaz09DB_TR.pdf
Vincent
Delaitre
Yevgeny
Kazakov
inproceedings
DelKaz:09:SQL:OWLED
Classifying <prt>ELH</prt> Ontologies In <prt>SQL</prt> Databases
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:Regularity:DL
An Extension of Regularity Conditions for Complex Role Inclusion Axioms
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
techreport
KazP-H:08:Graded:TR
A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics
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
arxiv.org
http://arxiv.org/abs/0905.3108
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2008/KazPH08Graded_TR.pdf
<prt>&tring; arXiv:0905.3108v1</prt>, posted on <prt>&tring; http://arxiv.org</prt>
Yevgeny
Kazakov
Ian
Pratt-Hartmann
inproceedings
KazakovPrattHartman:09:Graded
A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics
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:08:RIQ:SROIQ
<prt>RIQ</prt> and <prt>SROIQ</prt> Are Harder than <prt>SHOIQ</prt>
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
inproceedings
Kazakov:08:SRIQ:SROIQ
<prt>SRIQ</prt> and <prt>SROIQ</prt> are Harder than <prt>SHOIQ</prt>
We identify the complexity of (finite model) reasoning in the DL SROIQ to be N2ExpTime-complete. We also prove that (finite model) reasoning in the DL SR---a fragment of SROIQ without nominals, number restrictions, and inverse roles---is 2ExpTime-hard.
2008
Description Logics
353
CEUR-WS.org
CEUR Workshop Proceedings
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2008/Kaz08SROIQ_DL.pdf
Yevgeny
Kazakov
article
KazMot:08:SHOIQ:JAR
A Resolution-Based Decision Procedure for <prt>SHOIQ</prt>
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
Modular Reuse of Ontologies: Theory and Practice
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
GlimmKazakov:08:RoleConjunctions
Role Conjunctions in Expressive Description Logics
We show that adding role conjunctions to the Description Logics (DLs) SHI and SHOIF causes a jump in the computational complexity of the standard reasoning tasks from ExpTime-complete to 2ExpTime-complete and from NExpTime-complete to N2ExpTime-hard respectively. We further show that this increase 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
LPAR
5330
Springer
Lecture Notes in Computer Science
391-405
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2008/GliKaz08RoleConjunctions.pdf
Birte
Glimm
Yevgeny
Kazakov
techreport
GliKaz:08:RoleConjunctions:TR
Role Conjunctions in Expressive Description Logics
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
The University of Oxford
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2008/GliKaz08RoleConjunctions_TR.pdf
Birte
Glimm
Yevgeny
Kazakov
techreport
KazSatZol:07:RBox
Is Your RBox Safe?
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:Safe
Ontology Reuse: Better Safe than Sorry.
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
inproceedings
CueHorKazSat:07:Modules
Just the Right Amount: Extracting Modules from Ontologies.
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:Framework
A Logical Framework for Modularity of Ontologies.
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
KazSatZol:07:NonSimple
How Many Legs Do <prt>I</prt> Have? <prt>N</prt>on-Simple Roles in Number Restrictions Revisited
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 demon-strate 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
inproceedings
CueHalKaz:07:Incremental
History Matters: Incremental Ontology Reasoning Using Modules
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
techreport
GrauHorrKazSatt:07:Modul:TR
Extracting Modules from Ontologies: Theory and Practice
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.
Research Report
2007
The University of Manchester
Oxford Road, Manchester M13 9PL, UK
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2007/CueHorKazSat07Modul_TR.pdf
Bernardo
Cuenca Grau
Ian
Horrocks
Yevgeny
Kazakov
Ulrike
Sattler
inproceedings
CueHorKazSat:07:Extracting
Extracting Modules From Ontologies: A Logic-based Approach
2007
OWL: Experiences and Directions 2007 (OWLED 2007)
Innsbruck, Austria
http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-258/
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2007/CueHorKazSat07Extracting.pdf
Bernardo
Cuenca Grau
Ian
Horrocks
Yevgeny
Kazakov
Ulrike
Sattler
inproceedings
KazakovMotik:06:SHOIQ
A Resolution-Based Decision Procedure for <prt>SHOIQ</prt>.
We present a resolution-based decision procedure for the description logic SHOIQ---the logic underlying the Semantic Web ontology language OWLDL. Our procedure is goal-oriented, and it naturally extends a similar procedure for SHIQ, which has proven itself in practice. Applying existing techniques for saturation-based decision procedures to SHOIQ is not straightforward due to nominals, number restrictions, and inverse roles---a combination known to cause termination problems. We overcome this difficulty by using the basic superposition calculus, extended with custom simplification rules.
2006
IJCAR
4130
Springer
Lecture Notes in Computer Science
662-677
10.1007/11814771_53
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2006/KazMot06SHOIQ.pdf
Yevgeny
Kazakov
Boris
Motik
phdthesis
Kazakov:06:Phd
Saturation-Based Decision Procedures for Extensions of the Guarded Fragment
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
A Framework of Refutational Theorem Proving for Saturation-Based Decision Procedures
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
A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment.
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<prt>&</prt>issn=0302-9743<prt>&</prt>volume=3229<prt>&</prt>spage=372
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2004/Kaz04GF2N.pdf
Yevgeny
Kazakov
inproceedings
KazNiv:04:ResGFTG
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.
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<prt>&</prt>issn=0302-9743<prt>&</prt>volume=3097<prt>&</prt>spage=122
fileadmin/website_uni_ulm/iui.inst.090/Publikationen/2004/KazNiv04Res4GFTG.pdf
Yevgeny
Kazakov
Hans
de Nivelle
inproceedings
Kazakov:04:ResGFTG:DP
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.
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 Doctoral Programme
106
CEUR Workshop Proceedings
http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-106/06-kazakov.pdf
Yevgeny
Kazakov
unpublished
Kazakov:04:CombRes
Combining Resolution Decision Procedures
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 \url<prt>http://web.comlab.ox.ac.uk/oucl/work/yevgeny.kazakov/publications/</prt>
Yevgeny
Kazakov
techreport
KazNiv:04:ResGFTG:TR
Resolution Decision Procedures for the Guarded Fragment with Transitive Guards
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
Subsumption of concepts in <prt>DL</prt> <prt>FL</prt> for (cyclic) terminologieswith respect to descriptive semantics is <prt>PSPACE</prt>-complete
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
Subsumption of Concepts in <prt>FL0</prt> for (Cyclic) Terminologies with Respect to Descriptive Semantics is <prt>PSPACE</prt>-complete.
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