text: Efficiently querying Description Logic (DL) ontologies is becoming a vital task in various data-intensive DL applications. Considered as a basic service for answering object queries over DL ontologies, instance checking can be realized by using the most specific concept (MSC) method, which converts instance checking into subsumption problems. This method, however, loses its simplicity and efficiency when applied to large and complex ontologies, as it tends to generate very large MSCs that could lead to intractable reasoning. In this paper, we propose a revision to this MSC method for DL SHI , allowing it to generate much simpler and smaller concepts that are specific enough to answer a given query. With independence between computed MSCs, scalability for query answering can also be achieved by distributing and parallelizing the computations. An empirical evaluation shows the efficacy of our revised MSC method and the significant efficiency achieved when using it for answering object queries.
  @cite_28: OWL DL, a new W3C ontology language recommendation, is based on the expressive description logic @math . Although the ontology consistency problem for @math is known to be decidable, up to now there has been no known "practical" decision procedure, that is, a goal-directed procedure that is likely to perform well with realistic ontology derived problems. We present such a decision procedure for @math , a slightly more expressive logic than @math , extending the well-known algorithm for @math , which is the basis for several highly successful implementations.
  @cite_38: A fundamental problem in Description Logics (DLs) is satisfiability, the problem of checking if a given DL terminology T remains sufficiently unconstrained to enable at least one instance of a given DL concept C to exist. It has been known for some time that lazy unfolding is an important optimization technique in model building algorithms for satisfiability [2]. It is also imperative for large terminologies to be manipulated by an absorption generation process to maximize the benefits of lazy unfolding in such algorithms, thereby reducing the combinatorial effects of disjunction in underlying chase procedures [5]. In this paper, we propose a generalization of the absorption theory and algorithms developed by Horrocks and Tobies [6, 7]. The generalization, called binary absorption, makes it possible for lazy unfolding to be used for parts of terminologies not handled by current absorption algorithms and theory. The basic idea of binary absorption is to avoid the need to internalize (at least some of the) terminological axioms of the form
  @cite_14: 
  @cite_39: We develop a novel absorption technique for large collections of factual assertions about individual objects. These assertions are commonly accompanied by implicit background knowledge and form a knowledge base. Both the assertions and the background knowledge are expressed in a suitable language of Description Logic and queries over such knowledge bases can be expressed as assertion retrieval queries. The proposed absorption technique significantly improves the performance of such queries, in particular in cases where a large number of object features are known for the objects represented in such a knowledge base. In addition to the absorption technique we present the results of a preliminary experimental evaluation that validates the efficacy of the proposed optimization.
summary: A common direction of these optimization techniques is to reduce the high degree of nondeterminism that is mainly introduced by GCIs in the TBox: given an GCI @math , it can be converted to a disjunction @math , for which a tableau algorithm will have to nondeterministically choose one of the disjuncts for tableau expansion, resulting in an exponential-time behavior of the tableau algorithm w.r.t. the data size. Absorption optimizations @cite_28 @cite_38 @cite_14 were developed to reduce such nondeterminism by combining GCIs for unfoldable concepts, such that the effectiveness of lazy unfolding can be maximized. For example, axioms @math and @math can be combined into @math , where @math is a named concept; then the inference engine can deduce @math if the ABox contains @math . Notice however, this technique may allow only parts of TBox axioms to be absorbed, thus, may not be able to eliminate all sources of nondeterminism especially when ontologies are complex. Based on the absorption optimization, @cite_39 proposed an approach for efficient ABox reasoning for @math that will convert ABox assertions into TBox axioms, apply a absorption technique on the TBox, and covert instance retrieval into concept satisfaction problems.