Correcting Access Restrictions to a Consequence More Flexibly Eldora1? , Martin Knechtel2 , and Rafael Peñaloza1 1 Theoretical Computer Science, TU Dresden, Germany eldora.eldora@mailbox.tu-dresden.de, penaloza@tcs.inf.tu-dresden.de 2 SAP Research, Germany martin.knechtel@sap.com Abstract. Recent research has shown that labeling ontologies can be useful for restricting the access to some of the axioms and their implicit consequences. However, the labeling of the axioms is an error-prone and highly sensible task. In previous work we have shown how to correct the access restrictions if the security administrator knows the precise access level that a consequence must receive, and axioms are relabeled to that same access level. In this paper, we look at a more general situation in which access rights can be granted or denied to some specific users, without having to fully specify the precise access level. We also allow a more flexible labeling function, where the new access level of the relabeled axioms may differ from the level of the restriction. We provide black-box algorithms for computing suggestions of axioms to be relabeled. 1 Introduction Description Logics (DL) [1] have been successfully used to represent knowledge of various application domains. One of the main advantages of using a logic- based knowledge representation language is the possibility of reasoning within the system; that is, deriving implicit consequences from the explicitly stated knowledge in the ontology. In some application domains it is desirable to restrict users to access only portions of the ontology. For instance, in a security scenario [5], users with a low security clearance should not be able to access classified information. Other mo- tivations for restricting access to users are the reduction of information overload, or filtering w.r.t. a level of specialization. Rather than maintaining different sub- ontologies for each definable user level, we have previously proposed [2] to label each axiom with information on which users can access it. Reasoning then gener- alizes to the task of finding an adequate label for each implicit consequence of the ontology. This label, called a boundary, can be computed through black-box [2] as well as glass-box [9] techniques. However, the task of labeling axioms according to their access level is error- prone and highly sensitive to noise. Indeed, a set of seemingly innocuous axioms ? This work was developed while the author worked for SAP Research Dresden. may allow a user to derive some unwanted consequence. Dually, a too restrictive access level may hide a consequence from relevant users. This problem becomes more pronounced if neither the security administrator nor the knowledge engi- neer is an expert in logic. We thus want to develop a system that can automat- ically suggest changes in the labeling function that correct the access to a given consequence. In previous work [8, 7] we have developed and implemented efficient algo- rithms for correcting access restrictions to implicit consequences if (i) the knowl- edge engineer knows the exact access level the consequence must receive (called the goal label) and (ii) axioms are always relabeled to the goal label. In this paper we relax these both conditions. On the one hand, we allow the knowledge engineer to specify a bound on the desired access level, rather than an exact value. This is useful, for instance, to express that a set of users must all have access to the consequence, but it is irrelevant which other users (if any) can also derive it. On the other hand, the knowledge engineer is also able to specify a so-called target label to which the axioms are relabeled. Contrary to the previous approach, the target label needs not be equal to the goal label. We develop black-box algorithms for finding the minimal sets of axioms that need to be relabeled to the target label in order for the access of the consequence to satisfy the restriction imposed. Additionally, we show that our methods can be improved if one is only interested in finding one such set of minimal cardinality. All our methods are based on results and ideas from axiom-pinpointing [11, 3], but optimized by considering the labels of the axioms used. 2 Preliminaries To keep our presentation and results as general as possible, we impose only minimal restrictions to our ontology language. We just assume that an ontology is a finite set, whose elements are called axioms. An ontology language specifies which sets of axioms are admitted as ontologies, with the only restriction that every subset of an ontology is itself an ontology. If O0 ⊆ O and O is an ontology, then O0 is called a sub-ontology of O. A monotone consequence relation |= is a binary relation between ontologies O and consequences c such that if O |= c, then for every ontology O0 ⊇ O it holds that O0 |= c. If O |= c, we say that c follows from O or that O entails c. Consider, for instance, a description logic L. Then, an ontology is a finite set of general concept inclusion axioms (GCIs) of the form C v D, with C, D L-concept descriptions and assertion axioms of the form C(b), with C an L-concept description and b an individual name. An example of a consequence is the subsumption relation A v B between concept names A, B. If O |= c, we may be interested in finding the axioms responsible for this fact. A sub-ontology S ⊆ O is called a MinA for O,c if S |= c and for every S 0 ⊂ S, S 0 6|= c. The dual notion of a MinA is that of a diagnosis. A diagnosis for O,c is a sub-ontology S ⊆ O such that O \ S 6|= c and O \ S 0 |= c for all S 0 ⊂ S. L N For a lattice (L, ≤) and a set K ⊆ L, we denote as `∈K ` and `∈K ` the join (least upper bound) and meet (greatest lower bound) of K, respectively. We consider that ontologies are labeled with elements of the lattice. More formally, for an ontology O there is a labeling function lab that assigns a label lab(a) ∈ L to every element a of O. We will often use the notation Llab := {lab(a) | a ∈ O}. For a user labeled with the access level ` ∈ L, we denote as O≥` the sub- ontology O≥` := {a ∈ O | lab(a) ≥ `} visible for him. The sub-ontologies O≤` , O=` , O6=` , O6≥` , and O6≤` are defined analogously. Conversely, for a sub- ontology S ⊆ O, we define N L λS := a∈S lab(a) and µS := a∈S lab(a). An element ` ∈L L is join prime relative to Llab if for every K1 , . . . , Kn ⊆ Llab , it n holds that ` ≤ i=1 λKi implies that there is i, 1 ≤ i ≤ n such that ` ≤ λKi . For instance, in the lattice from Figure 1, `1 and `4 are the only elements that are not join prime relative to Llab = {`1 , . . . , `5 }, since `1 ≤ `2 ⊕ `4 but neither `1 ≤ `2 nor `1 ≤ `4 and similarly `4 ≤ `5 ⊕ `3 but neither `4 ≤ `5 nor `4 ≤ `3 . Join prime elements relative to Llab are called user labels. The set of all user labels is denoted as U . When dealing with labeled ontologies, the reasoning problem of interest consists on the computation of a boundary for a consequence c. Intuitively, the boundary divides the user labels ` of U according to whether O≥` entails c or not. Definition 1 (Boundary). Let O be an ontology, lab a labeling function and c a consequence. An element ν ∈ L is called a boundary for O,c,lab if for every join prime element relative to Llab ` it holds that ` ≤ ν iff O≥` |= c. Given a user label `u , we will say that the user sees a consequence c if `u ≤ ν for some boundary ν. The following lemma relating MinAs and boundaries was shown in [2]. Ln Lemma 2. If S1 , . . . , Sn are all MinAs for O,c, then i=1 λSi is a boundary for O,c. A dual result relating the boundary with the set of diagnoses, also holds. Nn Lemma 3. If S1 , . . . , Sn are all diagnoses for O,c, then i=1 µSi is a boundary for O,c. Example 4. Let (Ld , ≤d ) be the lattice shown in Figure 1, and O a labeled ontology from a marketplace in the Semantic Web with the following axioms a1 : EUecoService u HighperformanceService(ecoCalculatorV1 ) a2 : HighperformanceService v ServiceWithLowCustomerNr u LowProfitService a3 : ServiceWithLowCustomerNr v ServiceWithComingPriceIncrease a4 : EUecoService v ServiceWithLowCustomerNr u LowProfitService a5 : LowProfitService v ServiceWithComingPriceIncrease Fig. 1. Lattice (Ld , ≤d ) with 4 user labels and an assignment of 5 axioms to labels where the function lab assigns to each axiom ai the label `i as shown in Figure 1. This ontology entails ServiceWithComingPriceIncrease(ecoCalculatorV1 ). The MinAs for O,c are {a1 , a2 , a3 }, {a1 , a2 , a5 }, {a1 , a3 , a4 }, {a1 , a4 , a5 }, and its diag- noses are {a1 }, {a2 , a4 }, {a3 , a5 }. Using Lemma 3, we can compute the boundary as µ{a1 } ⊗ µ{a2 ,a4 } ⊗ µ{a3 ,a5 } = `1 ⊗ `1 ⊗ `4 = `4 . The join prime elements relative to Llab , which define valid user labels, are `0 , `2 , `3 , `5 . These labels represent the user roles as illustrated. Thus, the consequence c is only visible for the user roles `0 , `5 and `3 , i.e. for customer service employees, customers, and development engineers. 3 Modifying the Boundary An efficient implementation of a black-box algorithm for computing the bound- ary of DL consequences already exists [2]. However, a desirable addition to this method is the capability of automatically relabeling some of the axioms to cor- rect the access level of some implicit consequence. Indeed, labeling axioms w.r.t. their access restrictions is highly error-prone, and very small changes in the la- beling function may produce consequences to become visible to unauthorized users, or inaccessible to the relevant users. We have previously shown [8, 7] how to detect a set of axioms of minimal cardinality that needs to be relabeled for obtaining a given boundary. However, in that setting the knowledge engineer must specify the exact boundary that the consequence must receive, and all axioms are relabeled to that value. We now relax these restrictions, by allowing more general constraints on the new boundary, and a more flexible relabeling function. Definition 5 (Boundary Constraint, Change Set). A boundary constraint is a tuple β = (c, ∝ `g , `t ), where c is a consequence, ∝ `g , with ∝∈ {≤, ≥, 6≥, 6≤}, `g ∈ L is a condition and `t is the target label with `t ∝ `g . Let O be an ontology, S ⊆ O, lab a labeling function, and ` ∈ L. We define the modified labeling function labS,` as ( ` if a ∈ S, labS,` (a) = lab(a) otherwise. A sub-ontology S ⊆ O is called a change set (CS) for the boundary constraint β = (c, ∝ `g , `t ) if the boundary ν for O, c, labS,`t satisfies ν ∝ `g . For the rest of this paper, we assume, w.l.o.g. that the boundary for O, c, lab does not satisfy the condition ∝ `g since otherwise, the empty set is already a CS and nothing needs to be changed in the labeling function. Notice that, since `t ∝ `g , the whole ontology O is always a change set. However, using the whole ontology as a change set would set `t as the boundary of every consequence of O. In general, we want to make the least possible changes when correcting the boundary of a given consequence. For that reason, we will focus on finding all those change sets that are minimal w.r.t. set inclusion. These sets are useful if the knowledge engineer wants to obtain several suggestions of correction, and then choose the adequate one by some external criterion. However, due to the huge number (possibly exponentially many [4]) of change sets that may exist, one may also look for the “best” change set, and use it automatically in the correction. Hence, we also study how to find a smallest change set; that is, one with the least cardinality. We divide this section in two parts. First we look at the case where the bound- ary restriction is of the form ≤ or ≥. We show that previously known techniques can be used also in this setting. We then look at the negative restrictions, which require new methods to be developed. 3.1 Positive Conditions We now focus on the case where the condition of the boundary constraint is of the form ≥ `g . Due to the duality of MinAs and diagnoses, the case for ≤ `g can be treated in an analogous way (see e.g. [8]). Let β = (c, ≥ `g , `t ) be a boundary constraint and `t ≥ `g . Recall (Lemma 2) that the boundary can be computed as the supremum of all λSi , where Si is a MinA for O, c. Thus, if we relabel all the axioms in a MinA S to `t , then the boundary for O, c, labS,`t is ≥ `t ≥ `g ; that is, every MinA is a change set. Yet, this change set may not be minimal. In fact, we only need that the infimum of the labels of all the axioms in this MinA is ≥ `g . This can be achieved by only relabeling the axioms in S that are not already ≥ `g . Example 6. Continuing Example 4, recall that we have computed the label `4 as the boundary of the consequence c. Suppose now that we want to change this boundary to be ≥ `2 , using `2 also as the relabeling target. As described above, every MinA is also a change set for this consequence. If we consider the MinA S = {a1 , a2 , a3 }, then under the new labeling labS,`2 we obtain the new boundary λ{a1 ,a2 ,a3 } ⊕ λ{a1 ,a2 ,a5 } ⊕ λ{a1 ,a3 ,a4 } ⊕ λ{a1 ,a4 ,a5 } = `2 ⊕ `0 ⊕ `3 ⊕ `0 = `2 . However, it is easy to see through a simple computation, that the set {a3 } is also a change set, which is strictly included in the previous MinA. This set is obtained from the MinA by removing all axioms whose label is greater or equal `2 , namely a1 and a2 . Intuitively, we simply consider every axiom a ∈ O with lab(a) ≥ `g as fixed in the sense that its label cannot be changed, as changing it will be superfluous for any CS. We thus consider a generalization of MinAs, called IAS. Definition 7 (IAS). A minimal inserted axiom set (IAS) for ` is a subset I ⊆ O such that O≥` ∪ I |= c and O≥` ∪ I 0 6|= c for all I 0 ⊂ I. The known algorithms for computing all MinAs [6, 12] through a hitting set tree (HST) method [10] can easily be adapted for also computing IAS [8]. More interestingly, the set of all minimal change sets corresponds to the set of all IAS. Theorem 8. Let O be an ontology, β = (c, ≥ `g , `t ) a boundary constraint and S ⊆ O. S is a minimal CS for β iff S is an IAS for `g . In [8, 7] it is shown how to compute the set of all IAS for a consequence c. Moreover, the algorithms presented there have been also optimized for finding the smallest IAS, through the inclusion of a cardinality restriction. Basically, the construction of an IAS stops once that this has reached the cardinality of the smallest IAS found so far. It was shown that using these (partial) IAS can drastically reduce the search space, while preserving correctness of the method. Due to Theorem 8, all the algorithms for computing IAS and IAS of minimal cardinality can be used for finding the minimal change sets and a change set of minimal cardinality, for positive boundary constraints. 3.2 Negative Conditions We now consider the case in which the boundary constraint has a condition of the form 6≥ `g . As in the previous section, the case for 6≤ `g can be solved dually by simply interchanging MinAs and diagnoses. Given an ontology O, a labeling function lab and a consequence c, if the boundary for O, c, lab is greater or equal to `g , then we know that for every diagnosis S for O, c it holds that µS ≥ `g (see Lemma 3). Hence, if we relabel all the axioms in any diagnosis S to `t 6≥ `g , it follows that the boundary is then changed to a new value 6≥ `g ; that is, S is a CS. However, just as in the previous section, this CS may not be minimal. One idea to try to find a minimal CS is to follow the same intuition as in the previous section, and fix all axioms whose labels already satisfy the condition 6≥ `g . Unfortunately, this idea is not correct, as shown by the following example. Example 9. Returning to Example 4, suppose now that we want to change the boundary from `4 to some value 6≥ `4 , using `5 as a target label. Recall that {a2 , a4 } and {a3 , a5 } are diagnoses for the consequence. If we consider the axioms having a label 6≥ `4 as fixed, then none of these diagnoses produces a change set. In the first one, the axiom a2 would be fixed, but then, under the relabeling lab{a4 },`5 we will obtain the boundary µ{a1 } ⊗ µ{a2 ,a4 } ⊗ µ{a3 ,a5 } = `1 ⊗ (`2 ⊕ `5 ) ⊗ (`3 ⊕ `5 ) = `1 ⊗ `1 ⊗ `4 = `4 , Algorithm 1 Compute one minimal CS contained in a diagnosis Procedure compute-one-CS(S, β) Input: S: diagnosis; β = (c, 6≥ `g , `t ): boundary constraint; Output: T ⊆ S: minimal CS for β contained in S 1: if `t ≥ `g then 2: return ∅ 3: T := S 4: ` := `t 5: for every a ∈ S do 6: if ` ⊕ lab(a) 6≥ `g then 7: T := T \ {a} 8: ` := ` ⊕ lab(a) 9: return T which does not satisfy the restriction 6≥ `4 ; hence, {a4 } is not a change set. In the case of the second diagnosis, the problem is even greater, since both axioms will be considered as fixed. Thus, the approach would deduce that no axiom needs to be relabeled to obtain a boundary 6≥ `4 , which is obviously not true. Despite this, it is still possible to use diagnoses as a basis for computing the minimal CS. Suppose that we have a diagnosis S containing an axiom a0 such that `t ⊕ lab(a0 ) 6≥ `g . Then, S 0 = S \ {a0 } is also a CS, since M labS 0 ,`t (a) = `t ⊕ lab(a0 ) 6≥ `g . a∈S Lholds not only for a single axiom a0 but for any subset T Obviously, this result of S such that `t ⊕ a∈T lab(a) 6≥ `g . Lemma 10. Let S be a diagnosis for O, c and L β = (c, 6≥ `g , `t ) a boundary constraint. If T is a subset of S such that `t ⊕ a∈T lab(a) 6≥ `g , then S \ T is a CS for β. Proof. L For every axiom a ∈ S \ T , labS\T ,`t (a) = `t . Additionally, we know that a∈S lab(a) ≥ `g , and hence T = 6 S. Thus, under the new labeling, we have that M M labS\T ,`t (a) = `t ⊕ lab(a) 6≥ `g a∈S a∈T Since S is a diagnosis, Lemma 3 implies that the new boundary satisfies the condition, and hence S \ T is a CS. t u A simple consequence L of this lemma is that, given a maximal subset T of S satisfying `t ⊕ a∈T lab(a) 6≥ `g , S \ T is a minimal change set for β contained in S. Algorithm 1 describes how to compute one such minimal change set from a diagnosis. This, however, might not be a “globally” minimal change set; that is, there might still exist other change sets strictly contained in it, as shown in the following example. Example 11. Consider the lattice in Figure 1, an ontology O having four axioms {a1 , a2 , a3 , a4 }, and a consequence c such that the diagnoses for O, c are the sets {a1 , a2 , a3 } and {a1 , a4 }. Assume that the labeling function lab is given by the mapping lab(a1 ) = `4 , lab(a2 ) = `5 , lab(a3 ) = lab(a4 ) = `2 . It is easy to see that the boundary for this consequence is `1 . If we apply Algorithm 1 to the diagnosis {a1 , a2 , a3 } and the boundary constraint β = (c, 6≥ `1 , `3 ), where at Line 5, we first choose a3 , then ` is changed to `2 at Line 8, and hence the test `⊕lab(a) 6≥ `1 fails for axioms a1 and a2 . Thus, the algorithm returns the change set {a1 , a2 }. However, {a1 } is also a change set, since if a1 is relabeled to `3 , then µ{a1 ,a4 } = `2 ,and thus the boundary is 6≥ `1 . Although Algorithm 1 does not always output a globally minimal change set, one can still use it for computing all the minimal change sets for β. The idea is based on the following lemma, which is a simple consequence of the definition of diagnoses and change sets. Lemma 12. Let S be a minimal L change set for (c, 6≥ `g , `t ). Then, there exists a set T such that (i) `t ⊕ a∈T lab(a) 6≥ `g and (ii) S ∪ T is a diagnosis for O, c. For instance, in Example 11 we found the minimal change set {a1 }. The set T = {a4 } satisfies the two conditions stated in Lemma 12. To compute all minimal change sets, one then needs to compute all diagnoses, and from each of these diagnoses compute all the minimal change sets that are contained in it. This is possible through a nesting of two hitting set tree (HST) algorithms: the external one produces all different diagnoses for O, c, while the internal generates, for any given diagnosis, all the maximal subsets of axioms that can be removed to obtain a CS. Algorithm 2 shows how this internal HST algorithm works. The idea behind all HST-like algorithms is the following. One first computes a set of axioms T satisfying some property; in the case of Algorithm 2, the set is a minimal CS for β contained in S. This set is then used to label the root of the tree. The algorithm then branches as follows. For each axiom a in T , a new branch is created and a is removed from the search space. A new set T 0 satisfying the property is then computed, and used to label the successor node. The removal of the axiom a ∈ T from the search space ensures that T 6⊆ T 0 . This process is then iterated until the property is not satisfied by the search space; that is, Algorithm 1 returns the empty set. This process stops after at most exponentially many iterations, on the size of S, and the labels of the tree contain all the minimal sets of axioms satisfying the property; in our case, all minimal change sets contained in the diagnosis. There are two common optimizations for HST algorithms, which are also used in Algorithm 2. The first one is called early path termination. The idea behind this optimization is that if one can distinguish parts of the tree that will yield no new minimal sets of axioms, then one can stop exploring those branches. The two conditions for early path termination described in Line 1 of expand-hst test for a path where the search space is contained in a search space already explored in a Algorithm 2 HST to compute all minimal CS contained in a diagnosis Procedure compute-all-CS(S, β) Input: S: diagnosis; β = (c, 6≥ `g , `t ): boundary constraint; Output: C: all minimal CS for β contained in S 1: Global C, H := ∅ 2: T :=compute-one-CS(S, β) 3: C := {T } 4: for each a ∈ T do 5: expand-hst(S, (c, 6≥ `g , `t ⊕ lab(a)), {a}) 6: return C Procedure expand-hst(S, β, H) Input: S: diagnosis; β = (c, 6≥ `g , `t ): boundary constraint; H: list of axioms Side effects: modifications to C,H 1: if exists some H 0 ∈ H such that H 0 ⊆ H or H 0 contains a prefix path P with P = H then 2: return (early path termination) 3: T 0 := ∅ L 4: if exists some T ∈ C such that `t ⊕ a∈S\T lab(a) ∝ `g then 5: T 0 := T (CS reuse) 6: else 7: T 0 :=compute-one-CS(S, β) 8: if T 0 6= ∅ then 9: C := C ∪ {T 0 } 10: for each a ∈ T 0 do 11: expand-hst(S, (c, 6≥ `g , `t ⊕ lab(a)), H ∪ {a}) 12: else 13: H := H ∪ {H} (normal termination) previous branch. The second optimization is the reuse of sets. When expanding a tree, we only ask for a set of axioms satisfying the property that is contained in the current search space. If these conditions hold in a previously computed label, then we can reuse it, avoiding this way a possibly expensive call to Algorithm 1. To find all “global” minimal change sets, we use an additional HST algo- rithm that computes all diagnoses, and for each of these, calls Algorithm 2. This algorithm uses the same kind of optimizations. However, to improve the func- tionality of the reuse of solutions, the set of all change sets computed so far is kept in a global variable, accessible from every call to compute-all-CS. Thus, a change set that has been previously computed from a diagnosis S, can be reused in a call with a different diagnosis S 0 . It is worth noticing that in some cases, a diagnosis may contain several axioms labeled with the same lattice element. Moreover, the condition for obtaining a minimal CS from Lemma 10 depends only on the labeling, and not in the axiom itself. Thus, it is sometimes possible to optimize the search for the minimal CS by considering only the labels and not the individual axioms, as described in Algorithm 3. The correctness of this algorithm is justified by the following lemma, whose proof is analogous to the one of Lemma 10. Algorithm 3 Compute one minimal CS contained in a diagnosis (optimized) Procedure compute-one-CS(S, β) Input: S: diagnosis; β = (c, 6≥ `g , `t ): boundary constraint; Output: T ⊆ S: minimal CS for β 1: if `t ≥ `g then 2: return no CS 3: T := S 4: ` := `t 5: L := {lab(a) | a ∈ S} 6: for every m ∈ L do 7: if ` ⊕ m 6≥ `g then 8: T := T \ {a | lab(a) = m} 9: ` := ` ⊕ m 10: return T Lemma 13. Let S be a diagnosis for O, c, β = (c, 6≥ `g , `t ) a boundary L con- straint, and LS = {lab(a) | a ∈ S}. If M ⊆ LS is such that `t ⊕ `∈M ` 6≥ `g , then S \ {a | lab(a) ∈ M} is a CS for β. As in the case for positive conditions, these algorithms can be further op- timized if one is only interested in a change set of minimal cardinality. Notice simply that in Algorithms 1 and 3, whenever the condition in the for loop is violated, then at least an axiom is ensured to belong to the output change set. Thus, it is easy to adapt these algorithms to include a cardinality bound, return- ing a partial CS once it has reached a given size. Since our method uses an HST approach, the proofs of correctness of the variant of HST capable of exploiting cardinality restrictions [8] hold also in this case. In other words, Algorithm 2 can be further optimized to compute only one change set of minimal cardinality. 4 Conclusions We have presented algorithms for correcting the boundary of a consequence in a more flexible manner than previous approaches. Our framework allows the knowledge engineer to set bounds on what the new boundary should be, and specify a label as the target of the relabeling. This flexibility is useful if, for instance, she wants to grant access to a consequence to some user, but is not willing to specify the exact set of users that should access it. We developed algorithms that output all the minimal change sets. Addition- ally, we show how these algorithms can be optimized if one is only interested in an arbitrary change set of minimal cardinality. As future work, we will first implement and test the performance of our methods on large-scale real-world ontologies and applications. We also plan to generalize our framework to allow axioms to be relabeled to different elements of the lattice, according to an adequate minimality criterion. References 1. F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. F. Patel-Schneider, edi- tors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003. 2. F. Baader, M. Knechtel, and R. Peñaloza. A generic approach for large-scale onto- logical reasoning in the presence of access restrictions to the ontology’s axioms. In A. B. et al., editor, Proceedings of the 8th International Semantic Web Conference (ISWC 2009), Washington, DC, 2009. 3. F. Baader and R. Peñaloza. Axiom pinpointing in general tableaux. Journal of Logic and Computation, 20(1):5–34, February 2010. Special Issue: Tableaux and Analytic Proof Methods. 4. F. Baader, R. Peñaloza, and B. Suntisrivaraporn. Pinpointing in the description logic EL+ . In J. Hertzberg, M. Beetz, and R. Englert, editors, Proceedings of the 30th German Annual Conference on Artificial Intelligence (KI’07), volume 4667 of Lecture Notes in Artificial Intelligence, pages 52–67, Osnabrück, Germany, 2007. Springer-Verlag. 5. C. Farkas and S. Jajodia. The inference problem: a survey. SIGKDD Explor. Newsl., 4(2):6–11, 2002. 6. A. Kalyanpur, B. Parsia, M. Horridge, and E. Sirin. Finding all justifications of OWL DL entailments. In K. Aberer, K.-S. Choi, N. F. Noy, D. Allemang, K.-I. Lee, L. J. B. Nixon, J. Golbeck, P. Mika, D. Maynard, R. Mizoguchi, G. Schreiber, and P. Cudré-Mauroux, editors, Proc. of the 6th Int. Semantic Web Conf. and 2nd Asian Semantic Web Conf. (ISWC’07,ASWC’07), volume 4825 of LNCS, pages 267–280, Busan, Korea, 2007. Springer-Verlag. 7. M. Knechtel and R. Peñaloza. Correcting access restrictions to a consequence. In V. Haarslev, D. Toman, and G. Weddell, editors, Proceedings of the 2010 In- ternational Workshop on Description Logics (DL’10), volume 573 of CEUR-WS, Waterloo, Canada, 2010. 8. M. Knechtel and R. Peñaloza. A generic approach for correcting access restric- tions to a consequence. In L. Aroyo, G. Antoniou, E. Hyvönen, A. ten Teije, H. Stuckenschmidt, L. Cabral, and T. Tudorache, editors, Proceedings of the 7th Extended Semantic Web Conference (ESWC 2010), volume 6088 of Lecture Notes in Computer Science, pages 167–182, 2010. 9. R. Peñaloza. Using sums-of-products for non-standard reasoning. In A.-H. Dediu, H. Fernau, and C. Martı́n-Vide, editors, Proceedings of the 4th International Con- ference on Language and Automata Theory and Applications (LATA 2010), volume 6031 of Lecture Notes in Computer Science, pages 488–499. Springer-Verlag, 2010. 10. R. Reiter. A theory of diagnosis from first principles. Artificial Intelligence, 32(1):57–95, 1987. 11. S. Schlobach and R. Cornet. Non-standard reasoning services for the debugging of description logic terminologies. In G. Gottlob and T. Walsh, editors, Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI’03), pages 355–362, Acapulco, Mexico, 2003. Morgan Kaufmann, Los Altos. 12. B. Suntisrivaraporn. Polynomial-time Reasoning Support for Design and Mainte- nance of Large-scale Biomedical Ontologies. PhD thesis, Technische Universität Dresden, 2009.