Representation of context dependent knowledge in the Semantic Web is a recently emergent issue. A number of logical formalisms with this aim have been proposed [3, 11, 14]. Among them is the DL based Contextualized Knowledge Repository (CKR) [13]. One of the mostly advocated advantages of context based knowledge representation is that reasoning procedures can be constructed by composing local reasoners running inside each context, with the obvious divide-and-conquer advantage. We recently proposed a tableaux decision algorithm [5, 9] for the case of CKR framework based on ALC DL. The algorithm extends the well known ALC tableaux algorithm [6, 12] and it is based on a combination of local reasoning inside each context with a set of novel rules that propagate knowledge across the neighboring contexts. To our best knowledge, it is the only direct tableaux reasoning algorithm for contextualized DL knowledge to date: by direct we mean not based on some reduction to a single DL knowledge base, which neglects the divide-and-conquer advantage. In this paper, we review this algorithm and we describe our initial ideas on possible optimization, including dimensional coverage caching and parallelization. In order to maximize the divide-and-conquer advantage, it is important to propagate only those symbols between local tableaux which are really needed to assure completeness. We propose a (correctness preserving) modification of three propagation rules that decreases the amount of propagation and also of related non-deterministic branching. Proofs of all theorems can be found in the accompanying technical report [9].
We briefly introduce the basic definition of CKR, for all details see [13]. A meta vocabulary is used to state information about contexts. It contains contextual attributes (called dimensions), their possible values and coverage relations between these values. Formally, it is a DL vocabulary that contains: (a) a finite set of individuals called context identifiers; (b) a finite set of roles A called dimensions; (c) for every dimension A 2 A, a finite set of individuals DA, called dimensional values, and a role A, called coverage relation. The number of dimensions k = jAj is assumed to be a fixed constant.
Dimensional vectors are used to identify each context with a specific set of dimensional values. Given a meta-vocabulary with dimensions A = fA1; : : : ; Akg, a dimensional vector d = fAi1 :=d1; : : : ; Aim :=dmg is a (possibly empty) set of assignments such that for every j; h, with 1 j h m, dj 2 DAij , and j 6= h implies ij 6= ih. A dimensional vector d is full if it assigns values to all dimensions (i.e., jdj = k), otherwise it is partial. If it is apparent which value belongs to which dimension, we simply write fd1; : : : ; dmg. By dA (eA, etc.) we denote the actual value that d (e, etc.) assigns to the dimension A. The dimensional space D of is the set of all full dimensional vectors of .
An object-vocabulary, encodes knowledge inside contexts: it is a standard DL vocabulary (with disjoint sets NC of atomic concepts, NR of roles and NI of individuals) closed w.r.t. concept/role qualification. That is, for every concept or role symbol X of and every (possibly partial) dimensional vector d, a new symbol Xd is added to , called the qualification of X w.r.t. d. If d is partial then Xd is partially qualified, if d is full, it is fully qualified. Qualified symbols are used inside contexts to refer to the meaning of symbols w.r.t. some other context. This will become apparent from the semantics. Contexts and CKR knowledge bases are formally defined as follows. Definition 1 (Context). Given a pair of meta and object vocabularies h ; i, a context is a triple hC; dim(C); K(C)i where: C is a context identifier of ; dim(C) is a full dimensional vector of D ; and K(C) is an ALC knowledge base over . Definition 2 (Contextualized Knowledge Repository). Given a pair of meta and object vocabularies h ; i, a CKR knowledge base (CKR) is a pair K = hM; Ci where C is a set of contexts on h ; i and M, called meta knowledge, is a DL knowledge base over such that: (a) for A 2 A and d; d0 2 DA, if M j= A(C; d) and M j= A(C; d0) then M j= d = d0; (b) for C 2 C with dim(C) = d and for A 2 A, we have M j= A(C; dA); (c) the relation fhd; d0i j M j= d Ad0g is a strict partial order on DA. In the rest of the paper we assume that CKR knowledge bases are defined over some suitable vocabulary h ; i, and all concepts are in negation normal form (NNF, see [1]). We also assume the unique name assumption (UNA) for the meta knowledge (i.e., if a 6= b are two different symbols then M 6j= a = b). This is just to avoid the confusing possibility of two contexts located as the same place in the dimensional space.
For a CKR K, we will denote by Cd a context with dim(C) = d. For d; e 2 D and B; C A, dB := f(A:=d) 2 d j A 2 Bg is the projection of d w.r.t. B; and dB+eC := dB [ f(A:=d) 2 eC j A 2= Bg is the completion of dB w.r.t. eC.
An important notion is the strict ( ) and non-strict ( ) coverage between dimensional values: for d; d0 2 DA, d d0 if M j= d Ad0; and d d0 if either d d0 or M j= d = d0. Similarly, coverage for dimensional vectors: d B e for some B A if dB eB for each B 2 B; and d B e if d B e and dB eB for at least one B 2 B. Also, d e if d A e, and d e if d A e. Finally coverage for contexts: Cd Ce if d e, and Cd Ce if d e. Intuitively, if Cd Ce, then Cd is the narrower and Ce is the broader context.
An example CKR Kfb shown in Fig. 1 uses three dimensions time, location, and topic. It has four contexts associated with dimensional vectors sp (general context of sports in 2010), fb (football in 2010), wc10 (FIFA World Cup 2010), and n 10 (national football leagues in 2010). Axioms are placed inside each context while the associated vector is placed above it. Coverage relation is visualized with arrows.
Note that in CKR built on top of more expressive logics, conditions 2 (a,c) of Definition 2 can be assured directly in the meta knowledge with respective axioms: each A 2 A is declared functional, and each A is declared irreflexive and transitive. In ALC we do not have this option, however this is not a problem, because the number of all dimensions is assumed to be finite as it is the number of contexts in a CKR. Hence after the meta knowledge is modeled, these conditions can be verified even without a reasoner (e.g., by some script). These conditions are needed to assure reasonable properties of contextual space, i.e., acyclicity, dimensional values uniquely determined [13].
CKR uses DL semantics inside each context combined with some additional semantic restrictions to ensure proper meaning of qualified symbols. A partial DL interpretation of a DL vocabulary is a DL interpretation I = I ; I that allows two exceptions: I is possibly an empty set, and I is totally defined on NC and NR and it is partially defined on NI (i.e., aI 2 I can be undefined for some a 2 NI). Partial interpretations need not necessarily provide denotations for all individuals of . This is needed for technical reasons: intuitively, all contexts rely on the same object vocabulary , but some element of may not be meaningful in all contexts. Also, interpretations with empty domains are useful to treat inconsistency among contexts [13]. Definition 3 (CKR-Model). A model of a CKR K is a collection I = fIdgd2D partial DL interpretations (local interpretations) s.t. for all d; e; f 2 D , B A 2 NC, R 2 NR, X 2 NC [ NR, a 2 NI: 1. (>d)If (>e)If if d e 2. (Af )Id (>f )Id 3. (Rf )Id (>f )Id (>f )Id 4. aIe = aId if d e and – aId is defined or, – aIe is defined and aIe 2 d 9. Id j= K(Cd) 5. (XdB )Ie = (XdB+e)Ie 6. (Xd)Ie = (Xd)Id if d e 7. (Af )Id = (Af )Ie \ d if d 8. (Rf )Id = (Rf )Ie \ ( d
e d) if d of A, e The semantics takes care that local domains respect the coverage hierarchy (condition 1). Note that >d represents the domain of Id in the context where it appears. It gives rigid meaning to individuals, however, the meaning of an individual in a supercontext is independent if its meaning in a sub-context is undefined (condition 4). The interpretation of any Xf in any context Cd is roofed under (>f )Id (conditions 2, 3). The meaning of Xf in some context Ce is based on its context of origin Cf if this context is less specific than Ce (condition 6); otherwise, at least, any Xf in Cd and Ce must be equal on the shared part of their domains (conditions 7 and 8). Finally, each Id is a DL-model of Cd (condition 9). Albeit useful for modeling, partially qualified symbols are a kind of syntactic sugar in this framework as the completed version of the symbol can always be used instead (condition 5, cf. [13]). To simplify the algorithm, we assume w.l.o.g. that the CKR on the input is always fully qualified. In the examples we use non-qualified symbols only for improving readability.
Given a CKR K and d 2 D , a concept C is d-satisfiable w.r.t. K if there exists a CKR model I = fIege2D of K such that CId 6= ;; K is d-satisfiable if it has a CKR model I = fIege2D such that d 6= ;; K is globally satisfiable if it has a CKR model I = fIege2D such that e 6= ; for every e 2 D . An axiom is d-entailed by K (denoted K j= d : ) if for every model I = fIege2D of K it holds Id j= . As usual, d-entailment can be reduced to d-satisfiability: in particular K j= d : C v D iff C u :D is not d-satisfiable w.r.t. K. 3 We denote by clos(C) the set of all syntactically correct atomic and complex concepts that occur in a concept C. The closure of a concept C w.r.t. a CKR K is closK(C) = clos(C) [ fclos(:D t E) j D v E 2 K(C) for some context C of Kg [ fclos(D) j D(a) 2 K(C) for some context C of Kg [ fclos(:>e t >f ) j e f g. We denote with RK;C the set of roles R 2 NR appearing in C or some K(C) of K. The sets closK(C) and RK;C contain all possible concepts and roles relevant in order to verify d-satisfiability of C w.r.t. K.
The tableaux algorithm CT for CKR decides the d-satisfiability of a concept C w.r.t. a CKR K: it is partly based on the well known ALC tableaux algorithm [12, 6] which is extended in order to deal with multiple contexts. The algorithm works on a completion tree, a partial representation of a CKR model that the algorithm incrementally builds. Definition 4 (Completion tree). Given a CKR K, a completion tree is a triple T = hV; E; Li s.t.: 1. hV; Ei is a tree, where V is an ordered set of elements with order <V ; 2. there is a collection fVdgd2D of sets such that Vd V ; 3. Ed = fhx; yi 2 E j x; y 2 Vdg, for each d 2 D ; 4. L = fLdgd2D is a collection of labeling functions such that for each d 2 D : (a) Ld(x) closK(C), for each x 2 Vd; (b) Ld(hx; yi) RK;C , for each hx; yi 2 Ed.
In order to verify d-satisfiability of a concept C w.r.t. a CKR K, the algorithm initializes and then iteratively expands the tree using a number of tableaux expansion rules. To avoid infinite looping, a blocking policy adapted from Buchheit et al. [6] is used. We assume that the algorithm always adds nodes into the completion tree respecting the order <V (i.e., whenever a new node x is added, y <V x holds for all y already in V ). Definition 5 (Blocking). Given a CKR K and a completion tree T = hV; E; Li, we say that a node w 2 V is the witness for x 2 V , if Ld(x) = Ld(w) for all d 2 D , w <V x and there is no y 2 V such that y <V w and Ld(x) = Ld(y) for all d 2 D . We say that x 2 V is blocked by w 2 V if w is the witness for x.
We say that a tableaux rule is applicable if all of its preconditions (the if-part of the rule) are satisfied for some node x 2 V or a pair of nodes x; y 2 V and the nodes are not blocked. A completion tree T is complete, if none of the tableaux rules is applicable. A completion tree T = hV; E; Li contains a clash in a node x 2 V , if for some d 2 D and some concept C both C 2 Ld(x) and :C 2 Ld(x), or if ? 2 Ld(x). We say that T is clash-free if no clash occurs in any of its nodes.
In initialization, ABox axioms are encoded in the initial completion tree. This technique is well known for logics like ALC [1]. However, we must consider that in CKR same individuals appearing in different contexts may possibly have different meanings. In the completion tree, individuals will be represented by elements of the form ag where a 2 NI and g 2 D identifies the context in which the individual was first introduced. To implement condition 4 of CKR-models we will merge nodes when needed. Definition 6 (Merging). Executing merge(x; y) on a completion tree T = hV; E; Li, with x; y 2 V , transforms T as follows: a) node x is added into Ve for all e 2 D s.t. y 2 Ve; b) all concepts from Le(y) are added into Le(x), for all e 2 D ; c) all edges directed into/from y are redirected into/from x; d) node y is removed from V . Finally, the algorithm is formally defined as follows: Definition 7 (Algorithm CT ). Given as input a CKR K, d 2 D , and a concept C in NNF, the algorithm CT verifies the d-satisfiability of C w.r.t. K in the following steps:
The first five rules used by the algorithm (from u- to T -rule) are the usual ALC tableaux rules [1] responsible for local reasoning inside each context. The additional rules are new and they handle propagation of information between contexts.
The "- and #-rules are responsible for propagation of nodes: if d e, all nodes from Vd are propagated to Ve ( "-rule), but only the nodes belonging to >d are propagated from Ve to Vd ( #-rule).
Given contexts Cd and Ce, with d e, the conditions 6 and 7 of CKR-models require that the interpretations of any symbol Xf in the contexts agree on all elements shared by their domains. Hence, if a node (or a pair of nodes) belongs to both Vd and Ve (i.e. it belongs to both local tableaux), then its labels are propagated by A-rule and R-rule from one local tableaux to another, in both directions.
The following rules maintain the first three semantic conditions of CKR-models. The >A- and >R-rules take care that any qualified symbol Xd is always roofed under >d in any context Ce. If a qualified concept Ad (role Rd) is found in the Le-label of some node (edge) in Ve, then >d is added to the Le-label of this node (or both nodes connected by this edge). Also, if e f , then the >v-rule assures that the subsumption >e v >f must hold in any context. Finally, the M-rule takes care of cases when it is inferred that the same individual a appears in two different contexts.
It is however not the case that there is one-to-one correspondence between the semantic conditions of CKR (Definition 3) and the tableaux rules. Consider condition 6 and the case when Xd = Ad and d e. If for instance due to a firing of the 9-rule a new node x was added into Ve with Le(x) initiated to fAdg, to maintain condition 6 the same node with the same label must also be added to Vd and Ld respectively. This is achieved by consecutive firing of >A-, #-, and A-rules. A more complex example of reasoning with CKR tableaux rules follows.
Example 1 (Tableaux algorithm). Using the algorithm and our example CKR Kfb , let us show the proof for the following subsumption:
Kfb j= n 10 : WorldChampionPlayerfb v 8playsForwc10:WinnerTeamwc10
Initialization yields Vn 10 := fs0g and Ln 10(s0) := fWorldChampionPlayerfb u
9playsForwc10: :WinnerTeamwc10g. Then tableaux rules are applied as follows:
(
9playsForwc10::WinnerTeamwc10g by u-rule;
(
Ln 10(hs0; s1i) := fplaysForwc10g, Ln 10(s1) := f:WinnerTeamwc10g by 9-rule;
(
Lfb(hs0; s1i) := fplaysForwc10g by "-, A- and R-rules;
(
Lwc10(hs0; s1i) := fplaysForg by #-, A- and R-rules;
(
Ln 10(s1) := Ln 10(s1) [ fWinnerTeamwc10g by A-rule; The application of last rule creates a clash, since Ln 10(s1) = f:WinnerTeamwc10; WinnerTeamwc10g. Note that in the non-deterministic choices asked in steps 4 and 7 (due to t-rule), all other choices immediately lead to a clash. Hence no clash-free completion tree can be constructed and the algorithm answers that the input concept is n 10-unsatisfiable w.r.t. Kfb . This implies that the subsumption in question is entailed.
Note the required inter-contextual knowledge propagation: we first had to propagate nodes and their labels from Vn 10 to Vfb and finally to Vwc10 by tracking the context coverage structure (steps 3–6). Then with the last rule application (step 9), we propagate back the derived concepts to the label Ln 10 and detect the clash. 3 The algorithm CT is correct: it terminates on any input and it is sound and complete. Theorem 1 (Correctness). Given a CKR K, d 2 D , and a concept C in NNF on the input, the tableaux algorithm CT always terminates and C is d-satisfiable w.r.t. K iff CT generates a complete and clash free completion tree.
The ALC tableaux algorithm which we extended in this paper is in NEXPTIME [6], and this is the case also for the resulting tableaux algorithm for CKR.
Theorem 2 (Complexity). The complexity of the CT algorithm is NEXPTIME with respect to the combined size of the input.
In general, the problem of deciding d-satisfiability (and thus d-subsumption) in ALCbased CKR is EXPTIME-complete [4]. That is, the complexity is the same as for ALC with general TBoxes [1]. To obtain an optimal algorithm for CKR on top of ALC we would have to extend one of the EXPTIME algorithms for ALC (like, e.g., [7]). On the other hand, the algorithm presented in this paper is an important first step towards the algorithmic support for CKR based on more expressive DL (like SHIQ or SROIQ), since the tableaux algorithms for these logics can be seen as extensions of the basic ALC algorithm on top of which we have built. 4
In this section we share our initial ideas about optimization of the algorithm. CKR maintains a certain level of separation between meta and object knowledge (the former influences the latter but not vice versa). Object reasoning queries the meta knowledge only to verify the coverage between dimensional vectors. The number of contexts m is typically much smaller than the size of whole KB n and the number of dimensions k is assumed to be a constant, it hence makes sense to precompute3 the context coverage beforehand. This can be done within k m2 = O(m2) queries of the form M j= d A d0. Consequently, meta reasoning does not slow down object reasoning more than in other approaches with simpler meta knowledge representations [14].
One of the advantages of contextual reasoning is that the KB is split into smaller units and reasoning can be parallelized. Let us briefly sketch how this can be done with CKR. Reasoning in each context will be handled by a separate processor, which will exchange messages to deal with knowledge propagation. The computation time will be bounded by the context which requires the longest execution time together with the number of required messages. In this sense, the t-, u-, 9-, 8-, >A-, >R-, and >v-rules are locally executed. The remaining rules will be implemented as follows: "-, #-rules: the fact that a node has to be added into the target context is detected locally in the source context. A message is sent into the target context and this fact is also cached in the source context, which will be used by the other rules. A-, R-rules: thanks to caching of the information to which contexts nodes have been added, it can be locally detected that the concept and role labels of some node have to be propagated to the target context which is then done by a message. M-rule: note that if ag 2 Vd, ah 2 Ve, and d e, then eventually ag is added into Ve by the "-rule. Therefore also the precondition the M-rule can be locally verified and once detected, a respective message is sent to all other contexts.
Propagation of knowledge increases the number of messages and can trigger additional computation in the target context. It is hence desired to limit it to the necessary cases only. Using a technique similar to lazy unfolding [1], we were able to optimize the three tableaux rules >A, >R, and >v for propagation of the >e symbols as follows: >A-rule: >R-rule: >v-rule:
if x 2 Vf ; d e; Ad 2 Lf (x); >e 2= Lf (x) then Lf (x) := Lf (x) [ f>eg
if x; y 2 Vf ; d e; Rd 2 Lf (hx; yi); >e 2= Lf (x) \ Lf (y) then Lf (x) := Lf (x) [ f>eg; Lf (y) := Lf (y) [ f>eg
if x 2 Vf ; d e; :>e 2 Lf (x); :>d 2= Lf (x) then Lf (x) := Lf (x) [ f:>dg The main idea of these optimized rules is to avoid the introduction of a number of disjunctive concept expressions of the form :>d t >e caused by the >v-rule which could possibly cause unnecessary non-deterministic branching. Instead, we apply each disjunction only after one of the disjuncts is proven untrue.
Normally the >A-rule would add >d into the label of any node x in which Ad was found. Consequently, the >v-rule would be fired once for each e d and add :>d t >e every time. This eventually results into adding >e into the same label for each such e over the run of the algorithm. The optimized >A-rule skips the introduction of these disjunctions and directly adds the >e symbol for all such e. The >R-rule is also optimized in the very same fashion. Hence the two optimized rules >A- and >R-rule 3 This does not imply that a DL KB at meta level is useless. In meta knowledge modeling, DL axioms on dimensional values can constrain the coverage structure, e.g., given a location dimension, we can require cities to be located within some country: City v 9 location :Country. do the work previously done by the >A- and >R-rules but in addition they take care of the first part of the disjunction :>d t >e (i.e., the one which adds >e if >d was found). We still have to take care of the second part, and this is done by the >v-rule which adds :>d to any label in which :>e was found for d e.
The version of the algorithm CT that uses the >A-, >R-, and >v-rules instead of the >A-, >R-, and >v-rules respectively, will be denoted by CT .
Theorem 3 (Correctness of optimized rules). Given a CKR K, d 2 D , and a concept C in NNF on the input, the algorithm CT always terminates and C is d-satisfiable w.r.t. K iff CT generates a complete and clash free completion tree.
Example 2 (Optimized tableaux rules). Let us now compare the original tableaux rules with the optimized rules by the following deduction:
Kfb j= sp : TopSportsman v 8playsForwc10:WinnerTeamwc10
The algorithm is initialized with Vsp = fs0g and the label Lsp = fTopSportsmanu
9playsForwc10: :WinnerTeamwc10g. The original algorithm CT proceeds as follows:
(
Lsp(s1) = f:WinnerTeamwc10g by 9-rule;
(
The only other approach for reasoning with DL-based CKR is a translation from CKR into a single DL KB [13]. Unfortunately, this solution is not practically efficient, as the translation adds a large number of axioms in order to track complex relations between qualified symbols in a single KB. This is reflected also by a significant (cubic) blow up in the size of knowledge base after the translation. In contrast, a direct tableaux algorithm allows for more effective reasoning: local reasoning is executed in the respective part of the completion tree and only relevant consequences posed on other contexts are propagated into their respective tableaux labels, thus opening the possibility of parallelization. Our tableaux procedure is also related to the distributed tableaux algorithms for DDL [8] and P-DL [2], especially in the way how symbols are propagated between local tableaux. Apart from the fact that each of these algorithms implements a different semantics, our algorithm is also able to handle semantic dependencies between roles which is an open problem for DDL and P-DL so far.
Our newly introduced optimizations bring us near to approaches interested in parallelization of DL reasoning. One relevant approach in this area is presented in [10]. This work proposes a saturation procedure for the classification of the polynomial fragment E LHR+ of OWL 2 EL, distributable among multiple processors as a concurrent algorithm. The paper also presents an implementation in the reasoner ELK together with a promising evaluation over known E L ontologies. Even if the scope of [10] is different from our work, it highlights some aspects that support our approach. In particular, it shows that there is interest in a parallelized vision of DL reasoning algorithms. Moreover, it suggests that the sort of knowledge distribution and independence between contexts which we point to can effectively result in promising performance improvements. 6
Contextualized Knowledge Repository (CKR) is a knowledge representation framework that provides a contextual layer for DL knowledge bases. The recently introduced reasoning algorithm [5, 9] for ALC-based CKR provides the first direct tableaux decision procedure for contextualized knowledge. This solution is more effective than the previously known approaches based on reduction that lead to KB blow ups and loss of the divide-and-conquer advantage of contextual representation.
In this paper, we reviewed the algorithm and discussed on its possible optimization including dimensional structure caching, parallelization and a set of new rules that optimize the propagation of symbols among local tableaux. In the future we want to extend the algorithm towards more expressive DL such as SHIQ and SROIQ and formulate an EXPTIME algorithm based on the existing approaches [7]: we note that some of the optimizations (e.g. the lazy unfolding for >v or the precomputation of context coverage) can be easily adapted to different formulations of the algorithm. We will also study further optimizations for the propagation of qualified symbols.
Acknowledgements: This research was supported from the LiveMemories project. Martin Homola is also supported from the Slovak national project VEGA no. 1/1333/12.