Data and Knowledge Group

Yevgeny Kazakov: Publications

Journal Articles

Despoina Magka, Yevgeny Kazakov, and Ian Horrocks.
Tractable Extensions of the Description Logic EL with Numerical Datatypes.
JAR, 2011.
To appear.
[ BibTeX-Entry | Pdf (387K) ]

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.

Bernardo Cuenca-Grau, Christian Halaschek-Wiener, Yevgeny Kazakov, and Boontawee Suntisrivaraporn.
Incremental Classification of Description Logics Ontologies.
JAR, 44(4):337-369, 2010.
[ BibTeX-Entry | Pdf (454K) ]

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.

Yevgeny Kazakov and Boris Motik.
A Resolution-Based Decision Procedure for SHOIQ.
JAR, 40(2-3):89-116, 2008.
[ BibTeX-Entry | Pdf (321K) ]

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.

Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Modular Reuse of Ontologies: Theory and Practice.
JAIR, 31:273-318, 2008.
[ BibTeX-Entry | URL | Pdf (605K) ]

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.

Selected Conference and Workshop Publications

Frantisek Simancik, Yevgeny Kazakov, and Ian Horrocks.
Consequence-Based Reasoning beyond Horn Ontologies.
In IJCAI, pages 1093-1099, July 16-22 2011.
[ BibTeX-Entry | Pdf | Pdf (224K) ]

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.

Yevgeny Kazakov, Markus Krötzsch, and Frantisek Simancik.
Concurrent Classification of EL Ontologies.
In ISWC, 2011.
To appear.
[ BibTeX-Entry | Pdf (621K) ]

We describe an optimised consequence-based procedure for classificationofontologiesexpressedinapolynomialfragmentELHR+ 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.

Yevgeny Kazakov, Markus Krötzsch, and Frantisek Simancik.
Unchain My EL Reasoner.
In Riccardo Rosati, Sebastian Rudolph, and Michael Zakharyaschev, editors, Description Logics, volume 745 of CEUR Workshop Proceedings. CEUR-WS.org, 2011.
[ BibTeX-Entry | Pdf | Pdf (397K) ]

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 some preliminary experimental results analyzing when the restricted procedure can give practical improvements.

Birte Glimm, Yevgeny Kazakov, and Carsten Lutz.
Status QIO: An Update.
In Riccardo Rosati, Sebastian Rudolph, and Michael Zakharyaschev, editors, Description Logics, volume 745 of CEUR Workshop Proceedings. CEUR-WS.org, 2011.
[ BibTeX-Entry | Pdf | Pdf (300K) ]

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.

Yevgeny Kazakov, Markus Krötzsch, and Frantisek Simancik.
Concurrent Classification of EL Ontologies.
2011.
[ BibTeX-Entry | Pdf (646K) ]

We describe an optimised consequence-based procedure for classificationofontologiesexpressedinapolynomialfragmentELHR+ 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.

Despoina Magka, Yevgeny Kazakov, and Ian Horrocks.
Tractable Extensions of the Description Logic EL with Numerical Datatypes.
In IJCAR, volume 6173 of Lecture Notes in Computer Science, pages 61-75. Springer, 2010.
[ BibTeX-Entry | Pdf (231K) ]

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.

Yevgeny Kazakov.
An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ.
In IJCAR, volume 6173 of Lecture Notes in Computer Science, pages 472-486. Springer, 2010.
[ BibTeX-Entry | Pdf (353K) ]

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.

Despoina Magka, Yevgeny Kazakov, and Ian Horrocks.
Tractable Extensions of the Description Logic EL with Numerical Datatypes.
In Volker Haarslev, David Toman, and Grant Weddell, editors, Description Logics, volume 573 of CEUR Workshop Proceedings. CEUR-WS.org, 2010.
[ BibTeX-Entry | Pdf | Pdf (359K) ]

Vincent Delaitre and Yevgeny Kazakov.
Classifying ELH Ontologies In SQL Databases.
In OWL: Experiences and Directions 2009 (OWLED 2009), Chantilly, VA, United States, October 23-24 2009.
[ BibTeX-Entry | Pdf | Pdf (308K) ]

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.

Yevgeny Kazakov and Ian Pratt-Hartmann.
A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics.
In LICS, pages 407-416. IEEE Computer Society, August 11-14 2009.
[ BibTeX-Entry | Pdf (288K) ]

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.

Yevgeny Kazakov.
Consequence-Driven Reasoning for Horn SHIQ Ontologies.
In IJCAI, pages 2040-2045, July 11-17 2009.
[ BibTeX-Entry | Pdf (191K) ]

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.

Bernardo Cuenca-Grau, Boris Motik, and Yevgeny Kazakov.
Import-by-Query: Ontology Reasoning under Access Limitations.
In IJCAI, pages 727-732, July 11-17 2009.
[ BibTeX-Entry | Pdf ]

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.

Yevgeny Kazakov.
An Extension of Regularity Conditions for Complex Role Inclusion Axioms.
In Bernardo Cuenca-Grau, Ian Horrocks, Boris Motik, and Ulrike Sattler, editors, Description Logics, volume 477 of CEUR Workshop Proceedings. CEUR-WS.org, 2009.
[ BibTeX-Entry | Pdf | Pdf (192K) ]

Yevgeny Kazakov.
Consequence-Driven Reasoning for Horn SHIQ Ontologies.
In Bernardo Cuenca-Grau, Ian Horrocks, Boris Motik, and Ulrike Sattler, editors, Description Logics, volume 477 of CEUR Workshop Proceedings. CEUR-WS.org, 2009.
[ BibTeX-Entry | Pdf | Pdf (197K) ]

Birte Glimm and Yevgeny Kazakov.
Role Conjunctions in Expressive Description Logics.
In LPAR, volume 5330 of Lecture Notes in Computer Science, pages 391-405. Springer, 2008.
[ BibTeX-Entry | Pdf (1.9M) ]

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.

Yevgeny Kazakov.
RIQ and SROIQ Are Harder than SHOIQ.
In KR, pages 274-284. AAAI Press, 2008.
[ BibTeX-Entry | Pdf (2.6M) ]

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.

Yevgeny Kazakov.
SRIQ and SROIQ are Harder than SHOIQ.
In Description Logics, volume 353 of CEUR Workshop Proceedings. CEUR-WS.org, 2008.
[ BibTeX-Entry | Pdf (370K) ]

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.

Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Ontology Reuse: Better Safe than Sorry.
In Description Logics, pages 41-52, Brixen/Bressanone, Italy, June 8-10 2007. Bozen/Bolzano University Press.
[ BibTeX-Entry | URL | Pdf (181K) ]

Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Extracting Modules From Ontologies: A Logic-based Approach.
In OWL: Experiences and Directions 2007 (OWLED 2007), Innsbruck, Austria, June 6-7 2007.
[ BibTeX-Entry | URL | Pdf (168K) ]

Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Just the Right Amount: Extracting Modules from Ontologies.
In WWW, pages 717-726, Banff, Canada, May 2007. ACM.
[ BibTeX-Entry | URL | Pdf (380K) ]

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.

Yevgeny Kazakov, Ulrike Sattler, and Evgeny Zolin.
How Many Legs Do I Have? Non-Simple Roles in Number Restrictions Revisited.
In LPAR, volume 4790 of Lecture Notes in Computer Science, pages 303-317. Springer, 2007.
[ BibTeX-Entry | Pdf (266K) ]

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

Bernardo Cuenca-Grau, Christian Halaschek-Wiener, and Yevgeny Kazakov.
History Matters: Incremental Ontology Reasoning Using Modules.
In ISWC/ASWC, volume 4825 of Lecture Notes in Computer Science, pages 183-196. Springer, 2007.
[ BibTeX-Entry | Pdf (207K) ]

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.

Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
A Logical Framework for Modularity of Ontologies.
In IJCAI, pages 298-303, 2007.
[ BibTeX-Entry | Pdf | Pdf (131K) ]

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.

Yevgeny Kazakov and Boris Motik.
A Resolution-Based Decision Procedure for SHOIQ.
In IJCAR, volume 4130 of Lecture Notes in Computer Science, pages 662-677. Springer, 2006.
[ BibTeX-Entry | URL | Pdf (230K) ]

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.

Yevgeny Kazakov.
A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment.
In JELIA, volume 3229 of Lecture Notes in Computer Science, pages 372-384. Springer, 2004.
[ BibTeX-Entry | URL | PostScript [g-zip'd] (108K) | Pdf (203K) ]

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

Yevgeny Kazakov and Hans de Nivelle.
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.
In IJCAR, volume 3097 of Lecture Notes in Computer Science, pages 122-136. Springer, 2004.
[ BibTeX-Entry | URL | PostScript [g-zip'd] (98K) | Pdf (224K) ]

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

Yevgeny Kazakov.
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.
In IJCAR Doctoral Programme, volume 106 of CEUR Workshop Proceedings, 2004.
[ BibTeX-Entry ]

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

Yevgeny Kazakov and Hans de Nivelle.
Subsumption of Concepts in FL₀ for (Cyclic) Terminologies with Respect to Descriptive Semantics is PSPACE-complete.
In Description Logics, volume 81 of CEUR Workshop Proceedings, 2003.
[ BibTeX-Entry | PostScript [g-zip'd] (83K) | Pdf (154K) ]

We close the gap in the complexity classification of subsumption in the simple description logic FL₀, which allows for conjunctions and universal value restriction only. We prove that the subsumption problem in FL₀ 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

Yevgeny Kazakov.
Recursive resolution for modal logic.
In Proceedings of the Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, volume MPI-I-2002-2-007 of MPI Research Report, pages 11-15, Saarbrücken, Germany, March 2002. International Max Planck Research School for Computer Science (IMPRS), Max-Planck-Institut für Informatik.
[ BibTeX-Entry | PostScript [g-zip'd] (47K) ]

Resolution for the first order logic can be considered as a practical tool for obtaining a decision procedures for some theories (cf. [?]). For modal logics, however, there is no uniform formulation of the resolution principle, yet the normal modal logics are the most probable candidates to be decidable theories. The translational methods for modal logic, treated for instance in [?], yet possess some uniformness property, but does not let one to extract proofs from the refutations. On the other hand, direct methods (cf. [?], [?]) are local which gives not much practical use of them. This paper presents some arguments on generalization of the classical propositional resolution method to the language of modal logic. We give a resolution calculus for modal logic that inherits some features of classical resolution and propose some suggestions of how can it be used for other modal logics

Selected Technical Reports

Frantisek Simancik, Yevgeny Kazakov, and Ian Horrocks.
Consequence-Based Reasoning beyond Horn Ontologies.
Technical report, Oxford University, 2011.
[ BibTeX-Entry | Pdf (250K) ]

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.

Despoina Magka, Yevgeny Kazakov, and Ian Horrocks.
Tractable Extensions of the Description Logic EL with Numerical Datatypes.
Technical report, Oxford University, 2010.
[ BibTeX-Entry | Pdf (262K) ]

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.

Vincent Delaitre and Yevgeny Kazakov.
Classifying ELH Ontologies in SQL Databases.
Technical report, Oxford University, 2009.
[ BibTeX-Entry | Pdf (186K) ]

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.

Yevgeny Kazakov and Ian Pratt-Hartmann.
A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics.
Technical report, arxiv.org, 2009.
arXiv:0905.3108v1, posted on http://arxiv.org.
[ BibTeX-Entry | URL | Pdf (319K) ]

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.

Birte Glimm and Yevgeny Kazakov.
Role Conjunctions in Expressive Description Logics.
Technical report, The University of Oxford, 2008.
[ BibTeX-Entry | Pdf (2.3M) ]

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.

Yevgeny Kazakov, Ulrike Sattler, and Evgeny Zolin.
Is Your RBox Safe?
Research report, The University of Manchester, Oxford Road, Manchester M13 9PL, UK, July 2007.
[ BibTeX-Entry | Pdf (361K) ]

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.

Bernardo Cuenca-Grau, Ian Horrocks, Yevgeny Kazakov, and Ulrike Sattler.
Extracting Modules from Ontologies: Theory and Practice.
Research report, The University of Manchester, Oxford Road, Manchester M13 9PL, UK, February 2007.
[ BibTeX-Entry | Pdf (329K) ]

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.

Yevgeny Kazakov and Hans de Nivelle.
Resolution Decision Procedures for the Guarded Fragment with Transitive Guards.
Research Report MPI-I-2004-2-001, Max-Planck-Institut für Informatik, Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany, April 2004.
[ BibTeX-Entry | PostScript [g-zip'd] (249K) | Pdf (269K) ]

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

Yevgeny Kazakov and Hans de Nivelle.
Subsumption of concepts in DL FL₀ for (cyclic) terminologies with respect to descriptive semantics is PSPACE-complete.
Research Report MPI-I-2003-2-003, Max-Planck-Institut für Informatik, Stuhlsatzenhausweg 85, 66123 Saarbrücken, Germany, April 2003.
[ BibTeX-Entry | PostScript [g-zip'd] (137K) | Pdf (134K) ]

We prove the PSPACE-completeness of the subsumption problem for(cyclic) terminologies with respect to descriptive semantics in a simple Description Logic FL₀, which allows for conjunctions and universal value restrictions only, thus solving the problem which was open for more than ten years

S. Artemov, E. Kazakov, and D. Shapiro.
On logic of knowledge with justifications.
Technical Report CFIS 99-12, Cornell University, 1999.
[ BibTeX-Entry | PostScript [g-zip'd] (65K) ]

Drafts / To Appear

Yevgeny Kazakov.
A Framework of Refutational Theorem Proving for Saturation-Based Decision Procedures.
Research Report MPI-I-2005-2-004, Max-Planck-Institut für Informatik, on revison, August 2005.
[ BibTeX-Entry | Pdf (1.3M) ]

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, and give a computational model of the saturation process.

Yevgeny Kazakov.
Combining Resolution Decision Procedures.
unpublished manuscript, available from http://web.comlab.ox.ac.uk/oucl/work/yevgeny.kazakov/publications/, 2004.
[ BibTeX-Entry | PostScript [g-zip'd] (119K) | Pdf (254K) ]

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

Theses

Yevgeny Kazakov.
Saturation-Based Decision Procedures for Extensions of the Guarded Fragment.
PhD thesis, Universität des Saarlandes, Saarbrücken, Germany, March 2006.
[ BibTeX-Entry | Pdf (3.0M) ]

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