Abstract: In this study, we proposed a modular approach for description logic reasoning to meet the on-demand and scalability requirement semantic-based systems. One typical use of description logic knowledge-base is to support reasoning in semantic-based systems. However, including large description logic knowledge-bases in their complete form in applications would imply unnecessarily huge storage and computational requirement. Therefore, we go beyond the use of static description logic knowledge-base by reusing knowledge dynamically. In particular, we refer to the context-specific contents from large-scale description logic knowledge-bases as description logic modules. A tableau algorithm based on the description logic module representation is given to support modular description logic reasoning. In order to solve the semi-deterministic problem of modular reasoning, we propose an expansion reasoning algorithm for preserving consistency. We also analyzed the time complexity of the modular reasoning algorithm under different conditions. The proposed algorithm improved the performance of description logic reasoning by modulization, especially when the scale of the knowledge-base is very large.
INTRODUCTION
Recently, as a kind of knowledge representation system, Description Logics (DLs) (Brachman and Schmolze, 1985; Baader and Nutt, 2003) has become popular, with the emergence of the semantic web (Berners-Lee et al., 2001; Ilyas et al., 2004) and the research efforts of ontologies (Gruber, 1993; Van Heijst et al., 1997; Ding and Sun, 2009). Knowledge representation systems based on DLs provide users with various inference capabilities that deduce implicit knowledge from the explicitly represented knowledge. The study of suitable methods for solving the problems of reasoning in DLs has been developed starting with severe restrictions on the expressiveness of the language and on the form of the knowledge base. The original algorithm by Schmidt-Schauβ and Smolka (1991) for ALC as well as subsequent algorithms for more expressive DLs, could be seen as specializations of the tableau calculus for first-order predicate logic (Baader and Sattler, 2001). Tableau algorithms have turned out to be quite useful. They are complete and often of optimal complexity. The tableau-based approach has been developed and used as a mainstream solution to the reasoning problem in DLs.
However, including large-scale DL knowledge-bases in their complete form could incur an unnecessarily high storage and maintenance cost to semantic-based systems, especially when the capacity of a system is limited (e.g., an embedded system). As the size of a DL knowledge-base increases, the performance of the associated semantic-based systems will be quickly degraded as frequent search of knowledge is typically required. Therefore, it is important and urgent to share and reuse large-scale DL knowledge-bases to support semantic-based systems in a more efficient way.
By assuming that semantic-based systems typically need not the complete DL knowledge-base but just a portion of it, we propose to incorporate into systems the capability of knowledge-base modularization. In this study, we propose a modular approach of dynamic reasoning on large-scale DL knowledge-bases. We introduce the concept of DL module as well as the module cache for DL knowledge-base modularization. We present several modular reasoning algorithms based on the module representation. The proposed algorithm improves the performance of DL reasoning by modulization, especially when the scale of the knowledge-base is very large.
DL KNOWLEDGE-BASE MODULARIZATION
Here, we illustrated how to represent and manipulate modules formally based on the semantic structure of DL knowledge-base.
Definition: Generally, a DL knowledge-base K is a pair <T, A>, where T and A are its TBox and Abox. The TBox introduces the terminology like the vocabulary of an application domain while the ABox contains assertions about named individuals in terms of the vocabulary. The activities of many semantic-based systems rely only on localized information and knowledge as most applications have their specific contexts that they focus on (Ghidini and Giunchiglia, 2001). Our conjecture is that the activities of semantic-based systems need only specific aspects of a large-scale DL knowledge-base. The implication is that there is a need to provide semantic-based systems with the ability to modularize a large-scale DL knowledge-base according to requirements. Taking into account the locality of knowledge reference, we propose to represent those context-specific contents from a large-scale DL knowledge-base as DL modules (Mao et al., 2008). We give a formal definition of DL module to facilitate the discussion in the sequel as follows:
Definition 1 (DL Module): Given a DL knowledge-base K = <T, A>, a DL module (or module for short), M, is represented as a tuple <Mc, Mt, Ma, Mk>, where Mt ⊆ T, Ma ⊆ A, Mc = {DL concept ci}, where ∀ci∈T.
Mk is a reference to the DL knowledge-base K, which is also called the source of module. Mc contains some concepts from K and is called the concept set of the module. Given Mc, one can populate a corresponding module by searching the DL knowledge-base K for related concepts and storing them as Mt and Ma. <Mt, Ma > is called the knowledge set of the module and denotes a local knowledge-base. Note that Ma is a set of individuals from the ABox of the source DL knowledge-base, which makes the module be complete from the point of DL knowledge-base.
Given a DL module M = <Mc, Mt, Ma, Mk>, it has the following features:
| • | Completeness: Although M is a module from the source DL knowledge-base, it has a relatively complete local DL knowledge-base <Mt, Ma > |
| • | Connectivity: The concepts in Mt are connected. To a concept ci, in Mt, there is a relation between ci and cj, where cj is another concept in Mt |
Module manipulation: In order to facilitate manipulating modules from large-scale DL knowledge-bases, we also define a set of basic module operations as follows (Table 1):
We can manipulate modules from a large-scale DL knowledge-base efficiently with these operations. In a knowledge reuse framework, the operations can be packed as services, which are invoked by other semantic-based systems.
| Table 1: | The Operations for Manipulating Modules. |
Cache-based knowledge reuse: Compared with DL module, DL knowledge-base can be treated as static and invariant resource to semantic-based systems. Changes of DL knowledge-base require owner privilege and domain experts’ intervention, so it is unpractical to let semantic-based systems directly modify and update source DL knowledge-base. However, different systems can have their local repositories of modules from DL knowledge-base. Based on the module representation for DL knowledge-base, we propose to organize the modules of a semantic-based system in a local repository called module cache for dynamic knowledge reuse.
Definition 2 (Module cache): Given a DL knowledge-base K = <T, A>, a module cache, R, is represented as a triple <I, M, cv>, where M is a module from K, I is the index of M in R and cv is its cache value.
The concept of module cache draws inspiration from the memory caching mechanism. First emerging from data processing, caches work well because of a principle known as locality of reference. A module cache refers to a local repository for retrieved modules of DL knowledge-base for future reuse. Taking modules as cachable objects, module cache stores modules as cache blocks for knowledge reuse.
Caching the modules from a large-scale DL knowledge-base, which are frequently used in semantic-based systems, can improve the performance of semantic-based activities. When we want to use DL knowledge in applications, we first look for a module in a module cache providing formal semantics rather than accessing the source DL knowledge-base directly. For example, when a semantic-based system lacks the knowledge to perform a reasoning task, it needs to access the related DL knowledge-base. If the system has ever extracted the required modules and kept the most active ones in its module cache, the overall speed for reasoning is then optimized.
MODULAR DL REASONING
Reasoning for large-scale dl knowledge-base: One typical use of DL knowledge-base is to support reasoning of semantic-based systems (Donini and Lenzerini, 1996). Given a DL knowledge-base K = <T, A>, there are four major reasoning tasks (Baader and Nutt, 2003).
| • | Satisfiability: A concept C is satisfiable with respect to T if there exists a model I of T such that CI is nonempty. |
| • | Subsumption: A concept C is subsumed by a concept D with respect to T if CI ⊆ DI for every model I of T |
| • | Equivalence: Two concepts C and D are equivalent with respect to T if CI = DI for every model I of T |
| • | Disjointness: Two concepts C and D are equivalent with respect to T if CI ∩ DI = ø for every model I of T |
If, in addition to intersection, a DL system allows one to form the negation of a description, one can reduce other reasoning tasks to the satisfiability problem (Smolka, 1988; Schaerf, 1994). Therefore, we only consider the satisfiability problem and discuss the algorithm for satisfiability in this study.
Given an ALC-concept description, the tableau algorithm for satisfiability tries to construct a finite interpretation that satisfies the concept description. The original approach by Schmidt-Schaulβ and Smolka (1991) and many other studies on tableau algorithm for DLs, introduce the notion of a constraint system for this purpose. A satisfiability algorithm for ALC is presented as follows, based on the constraint systems (Schmidt-Schaulβ and Smolka, 1991) and the tableau algorithm for ALCN proposed by Buchheit et al. (1993). The transforming rules of the algorithm are shown in Table 2.
Given a concept description C0, we can construct an initial constraint system S0. Starting with S0, we thus,obtain a set of complete constraint systems {S1, S2, …, Sk} after a finite number of rule applications.
| Table 2: | The transforming rules of the satisfiability algorithm for ALC |
A constraint system Si is called complete iff none of the transformation rules applies to it. Consistency of a set of complete constraint systems can be decided by looking for obvious contradictions, called clashes.
Definition 3 (Clash): A constraint system Si contains a clash iff it has one of the following forms:
| • | {x:⊥} |
| • | {x:A, x:¬A}, where A is a concept name. |
| • | {x:≤n R} ∪ {<x, yi>:R |1≤i≤n+1} ∪ {yi ≠ yj |1≤ i≤ j≤ n+1}, where, R is a role name |
Any constraint system containing a clash is obviously unsatisfiable. If all constraint systems derived from S0 are unsatisfiable, then C0 is unsatisfiable. Otherwise, if there is a Si containing no clash, it is possible to construct a model and C0 is satisfiable (Buchheit et al., 1993).
Although, we are able to solve the reasoning problem of DLs by using the tableau algorithms, there is a gap between the reasoning services needed by large-scale DL knowledge-bases and those provided by the current systems. As a popular method for DL reasoning, tableau algorithm has a reasonable space complexity but with a high time complexity. Indeed, the algorithms based on tree-automata, which are used to prove EXPTIME-completeness, require exponential time even in simple cases. Donini and Massacci (2000) present a tableau calculus for checking the satisfiability of a concept with respect to a ALC-TBox with general axioms and transform it into the first simple tableau-based decision procedure working in single exponential time. The time complexity of the algorithm is O(2cn), for a suitable constant c>1, where n is the size of the input concept and the TBox. To a large-scale DL knowledge-base (e.g., a large-scale domain ontology), the size of the TBox is very large (n>10000). In that case, the cost of reasoning will be too high for real-life applications.
Therefore, how to implement efficient reasoning service for a large-scale DL knowledge-base is still a difficult issue to semantic-based systems. The knowledge involved in DL modules can be reused to support reasoning tasks above. In this study, we try to optimize the reasoning process by DL knowledge-base modularization.
Modular reasoning algorithm: In a system with the modularization mechanism, we can perform a DL reasoning task based on a module cache. The modules in a module cache are used as the local knowledge-bases for reasoning. We propose a modular DL reasoning algorithm based on the module representation. As mentioned before, we mainly consider the satisfiability problem in this study. Therefore, we try to solve the reasoning task of checking concept satisfiability in this algorithm. The reasoning Algorithm 1 is shown as follows:
| Algorithm 1: | DL reasoning algorithm based on module cache |
We illustrate the procedure of the algorithm as follows:
| Step 1: | Convert a concept description D into negation normal form (NNF) |
| Step 2: | Retrieve a matching module M from the module cache |
| Step 3: | Use DL reasoning algorithm to perform reasoning for D with the module M as the knowledge-base. The function DLReasoning refers to the process of DL reasoning by using a tableau algorithm |
| Step 4: | If no modules can be selected as the knowledge-bases for reasoning, perform a complete reasoning based on the source DL knowledge-base |
| Step 4: | Return the result of the reasoning |
In fact, the process of reasoning based on module is almost the same as that of DL knowledge-base. The only difference is the scale of the reasoning knowledge-base.
As the size of a module is far less than that of a large-scale DL knowledge-base, the complexity of the modular reasoning is also restricted to an acceptable extent. Therefore we decrease the complexity of DL reasoning by modularization.
To realize the function DLReasoning in Algorithm 1, we present a modular tableau algorithm for DL reasoning. The table algorithm is based on the algorithm mentioned earlier and tries to check the satisfiability of a concept description.
| Algorithm 2: | Modular tableau algorithm for DL reasoning |
We illustrate the procedure of the algorithm as follows:
| Step 1: | Convert the concept description D into negation normal form (NNF) |
| Step 2: | Construct an initial constraint system S based on D and the knowledge-base <Mt, Ma> of M |
| Step 3: | Apply the transforming rules in Table 2 to S and reduce it to generate new constraint systems; |
| Step 4: | If no more transforming rules are applicable to the constraint systems, terminate the reduction |
| Step 5: | If every constraint system in the resulted set contains a clash, it means that D is unsatisfiable. Otherwise, D is satisfiable |
If we take a module as the knowledge-base for DL reasoning, then the process of modular tableau reasoning is almost the same as that of a DL knowledge-base. For example, there is a DL knowledge-base Ktcm, which contains domain knowledge about Traditional Chinese Medicine (TCM). Ktcm, is a large-scale DL knowledge-base. The basic concepts and roles for this example are shown in Table 3.
In TCM, Chinese Materia Medica contains the natural medicinal materials used in TCM practice such as plants, animals and minerals, also known as herbal medicine. Formula of herbal medicine defines the basic notions and the theory of prescription. Here, glycyrrhiza, sargassum,angelica and tangerine peel are all herbal medicines.
| Table 3: | Some basic concepts and roles as well as their meanings |
Glycyrrhiza is an individual of legume and sargassum is an individual of gulfweed. Therefore, we have the following axioms in Ktcm:
| (1) |
| (2) |
| (3) |
| (4) |
| (5) |
| (6) |
| (7) |
According to the basic theory of TCM formula, glycyrrhiza and sargassum cannot be used as components in the same formula. Therefore, we have the following axiom in Ktcm:
| (8) |
A module cache is used to store DL modules extracted from Ktcm. Assume there are three modules M1 = <{Fga, Fst, Dg, Ds}, Mt1, ø, Ktcm>£¬M2 = <{F, Fg, Fs}, Mt2, ø, Ktcm>£¬M3 = <{F, D}, Mt3, ø, Ktcm> in the cache. Mt1 contains Eq. 1-3, 8. Mt2 contains Eq. 2-5, 8. Mt3 contains Eq. 1-7.
When a user forms a DL concept Fnew≡FgaΠFst, in order to represent a new kind of formula, it raises the problem of checking whether the concept description Fnew≡Fga Π Fst is satisfiable or not. We can use the modular reasoning algorithm to solve the problem.
With Algorithm 1, we first refer to the module cache and get the module M2 for modular reasoning. We assume Fnew is satisfiable and then it has one individual f at least. Therefore, we have an initial knowledge-base KB = {Mt2 ∪ {Fga Π Fst}, { Fga Π Fst(f)}} for reasoning. We can simplify some axioms in KB as follows:
| (9) |
| (10) |
| (11) |
| (12) |
| (13) |
| Fig. 1: | Example of checking concept satisfiability by using the modular tableau algorithm |
Then, we can construct an initial constraint system and perform reasoning according to Algorithm 2. The reduction process is shown in Fig. 1.
When the reduction is finished, we find that all branches are terminated with a clash and it means that every constraint system contains a clash. Therefore, the concept is unsatisfiable and the corresponding formula is a valid one in TCM.
Expansion reasoning: As a module from DL knowledge-base, a module only contains a small portion of knowledge of the complete knowledge-base. Therefore, the knowledge involved in a module is partial compared with its source DL knowledge-base. Assume that the TBox of a DL knowledge-base contains the following knowledge {C £ D,¬ C,∀R.D, EΠ F}. We extract a module M from the DL knowledge-base including the following knowledge {C£ D, R.D}. Given a concept description CΠD for checking satisfiability, we first perform modular reasoning based on the knowledge of M and get a positive answer. However, when we perform reasoning based on the source DL knowledge-base, we just get a clash (¬C and C) and the result is negative. Therefore, the result of modular reasoning is inconsistent with that of complete DL reasoning.
It is trivial to prove that modular reasoning based on module cache is semi-deterministic compared with DL reasoning. In order to keep consistent with the DL reasoning, we should improve Algorithm 1 further. We perform expansion reasoning when we get a positive result by modular reasoning. We propose an expansion reasoning algorithm for this purpose.
| Algorithm 3: | Expansion reasoning algorithm |
We illustrate the procedure of expansion reasoning as follows:
| Step 1: | To the conflict branches of modular reasoning, it is no need to expand it anymore |
| Step 2: | To each non-conflict branch, retrieve a matching module from the module cache (Fig. 2) |
| Step 3: | Perform modular reasoning based on the module |
Here, step 2 and 3 are performed recursively until no matching modules can be selected.
| Step 4: | When all the expansion reasoning processes are terminated with conflict, terminate the overall reasoning process. Otherwise, expand the reasoning to the whole source DL knowledge-base |
| Step 5: | Return the final result |
If we replace the input concept description Fnew≡Fga ΠFst with ∃R.¬D Π Fga, then the reduction process is different. We get the module M2 from the module cache for modular reasoning. The reduction process is shown in Fig. 3.
We get a constraint system without a clash after reduction. It means that ∃R.¬DΠFga is satisfiable with respect to M2. Then we have to perform expansion reasoning according to Algorithm 3. We get the module M2 from the module cache according to the final constraint system and perform modular reasoning. The reduction process is shown in Fig. 4.
When the reduction is finished, we find that all branches are terminated with a clash and it means that every constraint system contains a clash. Therefore, the concept is unsatisfiable and this result is consistent with that of Ktcm.
Although, the modular reasoning algorithm is semi-deterministic and we have to expand to the whole DL knowledge-base in the worst case, the modular reasoning algorithm does improve the performance of reasoning by modulization in some aspects. We will analyze the performance of the reasoning algorithm in detail later.
| Fig. 2: | The expansion reasoning for the modular reasoning algorithm |
| Fig. 3: | Example of the expansion reasoning (a) |
| Fig. 4: | Example of the expansion reasoning (b) |
COMPLEXITY ANALYSIS
Given an ALC knowledge-base K = <T, A> and a DL module M = <Mc, Mt, Ma, K>, the time complexity of the tableau algorithm with K is O(2cn), where n = nc + n1, nc is the size of the input concept and n1 is the size of T. The time complexity of the modular tableau algorithm (Algorithm 2) with M is O(2cm), where m = nc + n2, n2 is the size of Mt. We can analyze the time complexity of the modular reasoning under two different conditions:
| • | If the result of modular reasoning is negative, the result is consistent with that of complete DL reasoning. We can terminate the reasoning immediately. In this case, the time complexity for modular reasoning is O(2cm). As the size of Mt is much smaller than the size of T, it means n2 << n1 and O(2cn) << O(2cm). The time complexity of modular reasoning is much lower than that of DL reasoning in this case |
| • | If the result of modular reasoning is positive, the result is semi-deterministic. In order to keep consistent with the result of complete DL reasoning, we have to perform expansion reasoning. As the expansion procedure is linear, the time complexity is: |
where, ni is the size of the knowledge set of the ith module in the module cache for expansion reasoning. In the worst case, we have to expand the reasoning to the whole source DL knowledge-base and the time complexity is just O(2cn) in that case.
In summary, although the modular reasoning is semi-deterministic, the modular reasoning algorithm could decrease the complexity of reasoning for large-scale DL knowledge-base to some extent. This is mainly because that we reduce the problem space for reasoning by modularization.
DISCUSSION
There have been a number of on-going efforts in modular DL reasoning. Compared with our work, the related works to our approach can be broken down into the following categories: DL knowledge-base or ontology modularity and Modular DL reasoning.
The idea of extracting a subset of a large-scale DL knowledge-base or ontology is referred to by many different names: views, segments, modules, packages, partitions, etc. This research topic is mainly about segmenting or extracting modules from large-scale ontologies to satisfy application requirements. Noy and Musen (2004) defined a portion of an ontology as an ontology view and proposed an approach of specifying ontology views through traversal of concepts. Seidenberg and Rector (2006) proposed some algorithms for extracting relevant segments from large DL ontologies. They interpreted super-classes and quantified restriction as links between classes. Grau et al. (2006) defined the notation of locally correct and complete to capture the feature of ontology modularity. They presented an algorithm for automatically identifying and extracting modules from OWL-DL ontologies. Doran (2006) focused on ontology modularisation for reuse. They wanted to separate only part of an ontology, which was correct and self contained and could be reused instead of the original one. It can be concluded from the existing works that reusing large-scale DL knowledge-base by modules can improve the efficiency of semantic-based applications. The DL module presented in this paper is similar with the existing concepts. However, we propose a more formal definition for DL modules that can be reused in a variety of semantic-based applications.
Serafini et al. (2005) presented research on knowledge representation and reasoning that support modularity, scalability and distributed reasoning. They indicated a characterization of inferences using a cache-based implementation for local reasoners. Ding and Haarslev (2006) presented a tableau caching technique for SHI to improve the performance of tableau-based DL reasoners. Their results indicate a significant improvement in runtime performance once caching is enabled. Lin (2006) presented a tableau algorithm for concept satisfiability based on ontology modules. If the result is unsatisfiable, the reasoning can be terminated; otherwise, it is still doubtful and the reasoning should go on with the source ontology. Pan (2007) proposed a flexible reasoning architecture for OWL DL and described the prototype implementation of the reasoning architecture based on the FaCT DL reasoner. DL reasoners like RACE also caches concepts that have been reduced or knowledge about unsatisfiablity for future reuse (Horrocks and Schneider, 1999; Haarslev and Moller, 2000). Besides, some research efforts in distributed DLs (Borgida and Serafini, 2002) were concerned with tableau reasoning based on multiple ontology modules (Bao et al., 2006). However, the modules are from different knowledge-bases in that case. From the cases before-mentioned, it can be seen that we can improve DL reasoning by modularity. To contrast with existing research efforts, we propose a modular approach to improve the performance of DL reasoning. We enable semantic-based systems to reuse large-scale DL knowledge-base dynamically by modularization. Our concern of modular reasoning focuses on reasoning about a large-scale DL knowledge-base with a caching mechanism. We also consider the consistent problem between DL modules and the source DL knowledge-base in this study.
CONCLUSION
To semantic-based systems, the ability of reusing large-scale DL knowledge-bases is restricted by the computing and storage capacity of system. In this study, we present a modular approach for reusing large-scale DL knowledge-bases. We define the context-specific contents from large-scale DL knowledge-bases as modules. We combine the caching mechanism with DL knowledge-base reuse to form module cache. Semantic-based systems are able to use module caches as their local knowledge-bases to support semantic-based activities like DL reasoning. We mainly present a modular reasoning algorithm based on the module representation. The algorithm is able to improve the performance of DL reasoning, especially when the scale of the DL knowledge-base is large. There is still much room for improvement on the proposed approach. Future research issues include (1) extending the algorithm to satisfy more DL languages that are more complex than ALC and (2) considering the situation where modules are from different DL knowledge-bases to improve the algorithm.
ACKNOWLEDGMENTS
This work is partially supported by a grant from Educational Commission of Zhejiang Province (No. Y200908082) and a Science and Technology Program of ZJGSU (No. 1130KU110005).