Towards Parallel Repair: An Ontology Decomposition-based Approach? Yue Ma1 and Rafael Peñaloza1,2 1 Theoretical Computer Science, TU Dresden, Germany 2 Center for Advancing Electronics Dresden, Germany {mayue,penaloza}@tcs.inf.tu-dresden.de Abstract. Ontology repair remains one of the main bottlenecks for the development of ontologies for practical use. Many automated methods have been developed for suggesting potential repairs, but ultimately hu- man intervention is required for selecting the adequate one, and the human expert might be overwhelmed by the amount of information de- livered to her. We propose a decomposition of ontologies into smaller components that can be repaired in parallel. We show the utility of our approach for ontology repair, provide algorithms for computing this de- composition through standard reasoning, and study the complexity of several associated problems. 1 Introduction One of the main challenges in real-world Description Logic (DL) based applica- tions is to maintain the ontologies consistent with the intended domain modeling, a task often involving interactions with domain experts. It is thus desirable to allow experts to work distributively and in parallel for verifying and correct- ing unexpected logical consequences. This task is of a particular importance in scenarios where information is precious, large, and complex, and where manual verification of a repair plan is a necessary but labour-consuming task. Current research on ontology repair (see e.g. [5, 6, 8, 10, 15, 17, 20]) focuses on pinpointing the axiomatic causes, called MinAs of an unintended consequence and using them to compute a repair plan. For example, consider the ontology O = {A v Bi , Bi v C | 1 ≤ i ≤ n + 1} ∪ {Bi+1 v Bi | 1 ≤ i ≤ n}. Clearly, O implies A v C, and there are diverse reasons for this entailment: {A v Bi , Bi v C} and {Bi v C, Bi+1 v Bi , A v Bi+1 } for each i, 1 ≤ i ≤ n. This situation is depicted in Figure 1, where each axiom of O is represented with a node, and the different MinAs for A v C are surrounded by an ellipse. To repair the ontology, minimal hitting sets [18], represented with squared nodes in each subfigure from Figure 1, are the commonly used. The reason for ? This work is supported by the DFG Research Unit FOR 1513, project B1 and within the Cluster of Excellence ‘cfAED’. ··· ··· Fig. 1. Two minimal hitting sets (sets of squared dots) of the illustrative ontology O ··· Fig. 2. A decomposition of O (thickened circles) this choice is that a minimal hitting set of all MinAs corresponds to a minimal set of elements that need to be removed to avoid this consequence. That is, it provides a minimal repair plan, which can be computed automatically. When multiple experts are available for authenticating a repair plan, it would be desirable to divide this task in a manner that allows experts to work in par- allel. One way is to distribute one MinA to each expert. However, due to the overlaps between the MinAs, this may lead to unnecessary extra re-validations from different experts. Alternatively, we could distribute the minimal hitting sets; it is then unclear which hitting set should be sent from the many available. Consider the case where several hitting sets are precomputed and each one of them is sent to an expert. Besides the problem of possible overlaps among hitting sets in general, the large sizes of these sets (e.g. n + 1 in the example ontology O), means a high work load for each expert. Moreover, if a given hitting set is partitioned and distributed among different experts, there is a need of a com- munication mechanism for all experts to be informed of any decision made by the others, to avoid successive clashes and unnecessary effort. Based on these observations, we propose a novel methodology for decompos- ing ontologies that allows experts to validate and apply a repair plan in parallel. Generally speaking, we are interested in a decomposition that guarantees that: – no communication is required among experts and no axiom is submitted to more than one expert; and – the union of the repairs returned is free of the unintended consequence. For the example ontology O, a possible such decomposition is shown in Figure 2, where each thickened ellipse is a component delivered to an expert for repair. This decomposition allows n experts to work distributively, analysing two ax- ioms each. Stated in a general ontology language, our methodology is applicable to all logic-based applications that have a necessity to have experts assisting the repair process. Moreover, to keep the modeling convention of a domain, we assume that subontologies should be delivered in their original format. All these features distinguish the present work from the existing research efforts on ontol- ogy decompositions, such as ontology modularization [7], ontology masking [8], decompositions based on minimal unsatisfiable sets (MUSs) [9], and root and derived axioms for unsatisfiable concepts [12], among many others. Due to space limitations, all proofs are left in a technical report [14]. 2 Preliminaries To remain as general as possible, we do not fix any specific knowledge represen- tation formalism, but assume that we have an ontology language that describes two classes of well-formed formulas called axioms and consequences, respectively. An ontology O is a finite set of axioms, and a subset of O is called a subontology of O. For a fixed ontology language L, a monotone consequence relation |= is a binary relation between ontologies O and consequences α of L such that, if O |= α and O ⊆ O0 , then O0 |= α. If O |= α, we say that O entails α. For the rest of this paper, we denote as C the complexity of deciding entailments in L. Two examples of ontological languages are HL and EL, among other DLs [2]. In HL axioms and consequences are Horn clauses p0 ← p1 ∧ . . . ∧ pn , n ≥ 0, where each pi is a propositional variable 0 ≤ i ≤ n. In this case, the standard logical entailment relation ` is a monotone consequence relation. In EL, concepts are built from disjoint sets NC and NR using the rule C ::= A | > | C u C | ∃r.C, where A ∈ NC and r ∈ NR . Axioms and consequences in this logic are GCIs C v D, where C, D are concepts, and subsumption is a monotone consequence relation. In HL and EL, the consequence relation can be decided in polynomial time [1, 3, 4]. If an unwanted consequence α follows from an ontology, we are interested in repairing it, by finding an appropriate weaker ontology that does not entail α anymore. Formally, a repair for O w.r.t. α is an ontology R such that (i) R 6|= α, (ii) R is weaker than O; that is, for every consequence β, if R |= β, then O |= β, and (iii) R is a minimal change of O. We simply say a repair for O when the consequence is clear from context. If α is an erroneous consequence, then a repair describes a minimal change of O that removes it. The notion of minimal change depends on the ontological knowledge and the desired application. For example, one can define repairs to be maximal subontologies that avoid the consequence (see e.g. [13]) or allow for a more fine-grained decomposition of the axioms [8]. We remain as general as possible, and allow any notion to be considered. As there is typically more than one repair for any given consequence, usually a human expert is needed to identify the best one. To aid in the repair process, it is often helpful to identify the axiomatic causes of the consequence, called MinAs.3 Definition 1 (MinA). Let O be an ontology and α a consequence with O |= α. A subontology M ⊆ O is a MinA for O w.r.t. α if M |= α and for every M0 ( M, M0 6|= α. An axiom is said to be consequence-free w.r.t. α if it is not in any MinA for O w.r.t. α. When the consequence is clear from context, we simply call it free axiom. Our goal is to divide the ontology into different components that can be repaired in parallel. Since free axioms are never responsible for the occurrence of the erroneous consequence α, for the rest of the paper we assume that the ontology O does not contain any consequence free axiom w.r.t. α. 3 MinAs receive several names. They are e.g. called MUS in propositional logic, and MUPS [19] or justifications [8, 11] in DLs. 3 General Ontology Decompositions We now formalize the notion of parallel ontology repair via decompositions. We start with the ideal case where an ontology can be fully decomposed into different components and repaired in parallel. However, the existence of this case can not be guaranteed. Hence, we subsequently propose a series of ontology decompositions that do not necessarily partition the whole ontology, but still allow repairs to be performed independently on each component. Definition 2 (Perfect Partition). Given an ontology O and a consequence α, a perfect partition of O w.r.t. α is a partition Sn {K1 , . . . , Kn } of O such that, if Ri is a repair of Ki for i, 1 ≤ i ≤ n, then i=1 Ri is a repair of O w.r.t. α. In this case, the perfect partition has size n. A perfect partition provides a way to break down an ontology into multiple dis- joint subontologies that can be resolved independently, and the union of their repairs will lead to a repair of the whole ontology.4 This characterizes the intu- ition of repairing an ontoloy in parallel. Example 3. Let O = {A v Bi , Bi v C | 1≤i≤n} ∪ {A v Di , Di v C | 1≤i≤m}. The sets Ki = {A v Bi , Bi v C} and Li = {A v Di , Di v C}, produce a perfect partition of O w.r.t. A v C. Repairing each Ki and Li w.r.t. A v C leads to a repair of O w.r.t. the same consequence. In this example, the set of mutually disjoint MinAs produces a perfect partition of O. However, this is not true in general, as illustrated by the following example. Example 4. Consider the ontology O = {A v B1 , B1 v C, A v B1 u B2 , B2 v C}. M1 = {A v B1 , B1 v C} and M2 = {A v B1 u B2 , B2 v C} are two disjoint MinAs for A v C, and {M1 , M2 } is a partition of O. However, they do not form a perfect partition: {B1 v C} and {A v B1 u B2 } are repairs of M1 and M2 , respectively, but their union {B1 v C, A v B1 u B2 } is not a repair of O. The ontology O from this example does not have any perfect partition of size ≥ 2. Clearly, a perfect partition of size 1 always exists: the whole ontology itself is such one. Since only decompositions of size larger than 1 are meaningful for parallel repair, in the rest of the paper, by a perfect partition we mean its size is equal or greater than 2 unless explicitly stated otherwise. The following theorem provides a simple sufficient condition for an ontology to have a perfect partition. Proposition 5. Let M1 , . . . , Mn be all the MinAs of O w.r.t. a consequence α. If these MinAs are all pairwise disjoint, O has a perfect partition of size n. In general the condition of partitioning the ontology is too strong. In some cases, a decomposition of larger size can be obtained if some axioms are not included in any of the components. We formalize this idea next. 4 A subontology is the repair of itself if it does not contain a MinA. Definition 6 (Perfect Partial-Partition). A set of mutually disjoint subon- tologies {K1 , . . . , Kn } is a perfect partial partition of O w.r.t. a consequence α if Snit satisfies the following Sncondition: given repairs Ri of Ki for each i, 1 ≤ i ≤ n, i=1 R i is a repair for i=1 Ki w.r.t. α. To characterize these partial partitions, we introduce the notion of decomposi- tion. This is inspired by the work [9] and the insight that the different subon- tologies submitted to experts should be inner-connected, but outer-isolated. Definition 7 (Decomposition). Let O be an ontology entailing a consequence α. A decomposition of O w.r.t. α is a set D := {K1 ,...,Kn } of mutually disjoint subsets of O such Sn that: (i) for every i, 1 ≤ i ≤ n, Ki |= α, and (ii) for every MinA M for i=1 Ki w.r.t. α, there is an i, 1 ≤ i ≤ n with M ⊆ Ki . The decomposition D has size n, or is an n-decomposition; each Ki is a component of D; and Dn (O, α) denotes the set of n-decompositions of O w.r.t. the consequence α. Intuitively, the condition (i) characterizes the inner-connection such that each expert is assigned with a subontology containing some causes of the consequence. And the condition (ii) guarantees the outer-isolation as illustrated by the follow- ing example. Example 8. Consider again the ontology O and the MinAs M1 and M2 from Ex- ample 4. {M1 , M2 } is not a decomposition because there {A v B1 uB2 , B1 v C} is also a MinA contained in M1 ∪M2 , violating the condition (ii) of Definition 7. Suppose that M1 and M2 were distributed to two experts, which return the re- pairs B1 v C ∈ M1 and A v B1 u B2 ∈ M2 , respectively. Then, these repairs together would still entail the unwanted consequence. Theorem 9. If D is an n-decomposition, then D is a perfect partial-partition of size n. Theorem 9 tells that the inconsistencies in each component of a decomposition can be resolved distributively and the merged repair becomes consistent. Notice that the union of the components needs not to be the whole ontology, so a decomposition Sn defined Defintion 7 is not necessarily Sn a perfect partition. Let U = O \ i=1 Ki . If U 6= ∅, we cannot guarantee that i=1 Ri ∪U does not entail the consequence. Consider again the example from the introduction with n = 2. For the decomposition {K1 , K2 } with Ki = {A v Bi , Bi v C} for i = 1, 2, the axiom B2 v B1 ∈ U. The subontologies R1 = {B1 S v C} and R2 = {A v B2 } n are repairs for K1 and K2 , respectively. However, i=1 Ri ∪ U |= A v C. To solve this issue, one can either drop the unconfirmed axiom B2 v B1 because the other axioms that can form a MinA with it have been verified by experts; or, repeat the same process by constructing a new decomposition to resolve the remaining inconsistencies. To parallelize the effort of repairing the ontology, we are interested in decompositions of maximal size. The corresponding decision problem is the following. Problem: max-decom Input: an ontology O, a consequence α, an integer m Question: is there an m-decomposition of O w.r.t. α? As we show next, this problem can be solved using a special kind of decomposi- tion made of MinAs only. Definition 10 (MinA Decomposition). A decomposition D = {K1 ,...,Kn } of O w.r.t. α is a MinA decomposition if for every i, 1 ≤ i ≤ n, Ki is a MinA for O w.r.t. α. Lemma 11. O has an m-decomposition if and only if O has a MinA decompo- sition of size m. Based on this lemma, we can decide max-decom by guessing m disjoint subsets K1 , . . . , Km of O in polynomial time, and verifying that they form a MinA decomposition; that is, solving the following problem. Problem: is-(mina)-decom Input: ontology O, consequence α, D = {K1 , . . . , Km } Question: is D a (MinA) decomposition of O w.r.t. α? To decide this problem, we can guess a MinA M that violates the second con- dition of Definition 7. To verify that M is indeed a MinA, polynomially many entailment tests are required. Thus we get the following bound. Lemma 12. is-decom is in coNPC . This lemma provides only an upper bound for the problem; in particular, it also shows that is-mina-decom is in coNPC . In general, these upper bounds do not need to be tight. For example, in HL it is possible to decide in polynomial time whether the set D = {M1 , . . . , Mm } is exactly the set of all MinAs for an ontology O [16]. It is easy to S see that the set D is a MinA decomposition m iff D is the set of all MinAs for i=1 Mi . Thus, is-mina-decom for HL can be solved in polynomial time. However, it is still an open question whether the same holds for is-decom, or for the more expressive logic EL, or for other logics with polynomial time entailment problems. Algorithm 1 uses all these ideas to decide max-decom. The procedure not- mina receives as input an ontology O and a consequence α, and answers “yes” if O is not a MinA w.r.t. α. This is the case if either O 6|= α (line 18), or there is a strict subset of O that still entails α (line 17). The other two procedures perform a non-deterministic guess; max-decom guesses the components, while is-decom guesses a MinA that violates the second condition of Definition 7. Theorem 13. max-decom is in (Σ2P )C . In particular, this theorem shows that max-decom is in Σ2P for both HL and EL. As before, the bound needs not be tight; indeed, using the arguments described above, it is easy to see that this problem is in NP for HL. Algorithm 1 Deciding max-decom 1: procedure max-decom(O, α, m) 2: for 1 ≤ i ≤ m do 3: guess Ki ⊆ O 4: if not-mina(Ki , α) then return no 5: if Ki ∩ Kj = ∅ for all i, 1 ≤ i < j ≤ m then 6: return is-decom({K1 , . . . , Km }, α) 7: else return no 8: end procedure 9: procedure is-decom(D, S α) 10: guess M ⊆ K∈D K 11: if M * K for all K ∈ D then 12: return not-mina(M, α) 13: else return yes 14: end procedure 15: procedure not-mina(O, α) 16: for all t ∈ O do 17: if O \ {t} |= α then return yes 18: return O 6|= α 19: end procedure Algorithm 2 Deciding perfect-part 1: procedure full-decom(O, α, m) 2: for 1 ≤ i ≤ m do 3: guess Ki ⊆ O 4: if {K1 , . . . , Km } is a partition of O then 5: return is-decom({K1 , . . . , Km }, α) 6: else return no 7: end procedure We are mainly interested in decompositions of maximal size since they allow for a more efficient parallelization of the repairing procedure: each component can be repaired independently, and the properties of the decomposition guaran- tee that the union of these repairs does not entail the consequence. However, we are interested in finding a repair for the whole input ontology O, not just for those axioms appearing in the decomposition. As described before, ideally we would find a perfect partition of size n, for a given natural number n. Accord- ingly, we want to decide whether such a decomposition exists. Problem: perfect-part Input: an ontology O, a consequence α, an integer m Question: is there a perfect partition of O w.r.t. α of size m? Algorithm 2 describes a method for deciding perfect-part. In a nutshell, it guesses a partition D of O of size m, and then verifies, through a call to the Fig. 3. Two 5-decompositions: left a MinA decomposition; right a justified decompo- sition with minimal remain. procedure is-decom from Algorithm 1, that D is a decomposition. This yields the same complexity upper bound as for max-decom. Theorem 14. perfect-part is in (Σ2P )C . We can in general visualize the set of MinAs for a consequence α as a hypergraph GO,α . Every axiom in O is represented through a node, and every MinA is a hyperedge in this hypergraph. Consider the sub-hypergraph HO,α of GO,α that contains only nodes belonging to some hyperedge; i.e., where all free axioms have been removed. It is easy to see that there is a perfect partition of size m iff there are at least m maximally connected subgraphs of HO,α . This is usually not a desired behavior for parallelization, since the number of components will be usually small. For example, the ontology depicted in Figure 3 allows for a decomposition of size 5, but its only perfect partition has size 1. On the other hand, S if D is an n-decomposition of O w.r.t. α, then D is a perfect partition of K∈D K w.r.t. α of size n. To maximize the number of components, and hence the degree of paral- lelization, we are willing to ignore some axioms, as described by the notion of decomposition. However, we should try to submit to the experts as much in- formation from the original ontology as possible, to ensure an effective repair process. This will be the focus of the next section. 4 Maximally Informative Decompositions While MinA decompositions are useful for deciding the existence of a decompo- sition of a given size, they, by construction, ignore a large amount of axioms from the ontology. Consider again the example in Figure 3. The maximal size of a de- composition of this ontology is 5, as shown on the left-hand-side graph through a MinA decomposition. In total, the components contain only 10 out of the 16 axioms from the ontology. Moreover, there is a whole MinA for the consequence that is left out of the decomposition; even if all the components are corrected, the obtained ontology would still entail the error. On the right-hand-side, we can observe a decomposition of the same size 5, whose components extend those of the MinA decomposition, and uses 14 out of the 16 axioms. Algorithm 3 Finding a minimal remain decomposition 1: procedure find-min-rem-dec(O, α, m) 2: D ← find-decom(O, S α, m) 3: R ← K∈D K 4: for all t ∈ O \ R do 5: if perfect-part(R ∪ {t}, α, m) then 6: R ← R ∪ {t} 7: return find-perfect-part(R, α, m) 8: end procedure When we send a subontology for repair, it should be as informative as pos- sible, to ensure that no simple errors are ignored. Clearly, the less axioms that are removed to build the decomposition, the more information that is gathered and used during the parallel repair. Thus, we are interested in finding, among all decompositions of maximal size, those that include the most axioms possible. Definition 15 (Minimal Remain Decomposition). Let n S be a natural num- ber and O |= α. The remain of a decomposition D is O \ ( K∈D K). A de- composition D ∈ DnS(O, α) is aSminimal remain decomposition if there is no D0 ∈ Dn (O, α) with K∈D K ( K∈D0 K. In other words, a decomposition S D has minimal remain if it is not possible to decompose a proper superset of K∈D K in the same number of components. Consider again the example in Figure 3. The decomposition on the right-hand- side has a remain with two axioms. It is a minimal remain decomposition, since adding any of these two axioms would destroy the properties of decompositions. To find a minimal remain decomposition, we can recursively try to add axioms from the remainder of a previously known n-decomposition, until none can be added, as described in Algorithm 3. More precisely, let D be an n-decomposition, for instance, a MinA decomposition S of size n that was constructed through Al- gorithm 1, and let R = K∈D K; i.e., R is the complement of the remain of D. For each axiom t in the remain of D, we decide whether R ∪ {t} has a full n-decomposition. If so, then t is added to R. At the end of this iteration, R has a maximal subontology that allows for a perfect partition of size n. Any perfect partition of this subontology is hence guaranteed to have minimal remain. The internal subprocedure in lines 3 to 6 of Algorithm 3 can be easily adapted to verify that the decomposition D has minimal remain. Problem: is-min-rem-decom Input: ontology O, consequence α, D = {K1 , . . . , Km } Question: is D a minimal remain decomposition of O w.r.t. α? In the variant algorithm, one only has to check that R ∪ {t} has no perfect partition, for every t ∈ O \ R. If that is the case, then D has minimal remain. Theorem 16. is-min-rem-decom is in (Π2P )C . Fig. 4. A Pareto decomposition without minimal remain Notice that the decomposition obtained through Algorithm 3 may have no re- semblance with the first decomposition found at line 2. Indeed, the only require- ment is that there is a perfect partition of all the axioms used, which could differ greatly from the original one. In some cases, e.g. when the first decomposition was constructed from some specific MinAs that should remain connected, it is desirable to only add axioms to the existing components. Definition 17 (Pareto Decomposition). Given n ∈ N, O |= α, and decom- positions D, D0 ∈ Dn (O, α), D is contained in D0 , denoted by D ⊆ D0 if, for every K ∈ D there is a K 0 ∈ D0 such that K ⊆ K 0 . D is a Pareto decomposition if there is no D0 6= D with D ⊆ D0 . Clearly, every minimal remain decomposition is also Pareto. The converse, how- ever, does not hold. Consider the situation depicted in Figure 4, where the ellipses represent the different MinAs for a given consequence. This ontology can be de- composed into a perfect partition of size two, simply by considering its connected subgraphs. It is easy to see that the 2-decomposition D, where one component is formed by the diamond-shaped axioms, and the other by the triangle-shaped ax- ioms is a Pareto decomposition. However, the dot-shaped axiom is in the remain of D. This implies that D is not a minimal-remain decomposition. To find a Pareto decomposition, we can use the same ideas of Algorithm 3. We first find a decomposition, and then try to add each of the remaining axioms to one of the components, as long as this addition still yields a decomposition. It can also be restricted to decide whether an input decomposition is already Pareto or not. Notice, however, that in line 5 the algorithm for deciding Pareto decomposition does not need to verify whether a set of axioms accepts a full decomposition, but rather whether a set of subontologies forms a decomposition, which, as seen before, is a simpler problem. Thus, we have the following. Problem: is-pareto-decom Input: ontology O, consequence α, D = {K1 , . . . , Km } Question: is D a Pareto decomposition of O w.r.t. α? Theorem 18. is-pareto-decom is in NPC . We have considered decompositions that maximize the information stored in the components in two different ways: either by minimizing the elements that remain out of the decomposition, or by maximizing the components in a Pareto optimal manner. Notice, however, that some of the axioms included in a component might be irrelevant for the repair of that specific component. For that reason, we might also be interested in justified decompositions. Table 1. Instantiation of complexity results for decomposition to different DLs. Language Consequence |= is-dec max-dec perf-part is-min-rem-d is-pareto-d is-just-d C general general C coNP (Σ2P )C (Σ2P )C (Π2P )C NPC (Σ2P )C HL entailment P P NP NP coNP P NP EL subsumption P coNP Σ2P Σ2P Π2P NP Σ2P ALC consistency ExpTime ExpTime ExpTime ExpTime ExpTime ExpTime ExpTime Definition 19 (Justified Decomposition). Let O |= α. A decomposition D is called justified if for every K ∈ D and every t ∈ K there exists a MinA M of O w.r.t. α such that t ∈ M ⊆ K. Clearly, we can combine this notion with the previous ones and obtain, e.g., Pareto justified decompositions. All the algorithms presented so far can be eas- ily adapted to handle justified decompositions. One only needs to perform an additional check to verify that there is a full MinA for every axiom contained in a component. This test adds a new non-deterministic test, and hence the upper bounds increase to the next level of the polynomial hierarchy. Moreover, this jump in the hierarchy cannot be avoided since deciding whether an axiom is justified in a component is already NP-hard for very simple sublogics of HL [16]. 5 Conclusions We have introduced several notions of ontology decomposition targeted towards an efficient repair mechanism. Our motivating idea is that human experts, which are usually in demand for a correct repair of an ontology, can be easily over- whelmed by the amount of axioms provided to them. We thus suggest to divide the ontology into disjoint components that can be repaired in parallel, possibly by several different experts. Our definition of decomposition guarantees that the combination of the individual repairs for the components does not yield any new errors, hence providing an efficient parallelization of the repair process. We have mainly focused on studying the different decision problems associ- ated with decomposing ontologies, and their complexity. Our approach is general, considering an arbitrary monotonic consequence relation over some ontology lan- guage. Hence, our complexity analysis can only provide upper bounds; whether these bounds are tight or not is a matter of the specific language used. However, our results can be instantiated to well-known ontology languages. In Table 1 we summarize the complexity of these problems for DLs. The cells show the known upper bound for deciding the problems at each column; cells with a darker back- ground represent tight bounds. We plan to study the precise complexity of these problems for specific lan- guages, in particular for light-weight DLs. We will also further consider the applicability of our decompositions for practical ontology repair. To this goal, we will implement optimized versions of our algorithms and study the viability of developing a repair plan, in which components are sent to experts in a manner that minimizes the expected total effort and time required to remove the error. References 1. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence IJCAI-05. Morgan-Kaufmann Publishers, Edinburgh, UK (2005) 2. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applica- tions. Cambridge University Press, 2nd edn. (2007) 3. Brandt, S.: Polynomial time reasoning in a description logic with existential re- strictions, GCI axioms, and—what else? In: de Mantáras, R.L., L. Saitta (eds.) Proceedings of the 16th European Conference on Artificial Intelligence (ECAI- 2004). pp. 298–302. IOS Press (2004) 4. Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Log. Program. 1(3), 267–284 (1984) 5. Erdogan, H., Bodenreider, O., Erdem, E.: Finding semantic inconsistencies in umls using answer set programming. In: Fox, M., Poole, D. (eds.) Proc. of the 24th Nat. Conf. on Artificial Intelligence (AAAI’10) (2010) 6. Gebser, M., Schaub, T., Thiele, S., Veber, P.: Detecting inconsistencies in large biological networks with answer set programming. TPLP 11(2-3), 323–360 (2011) 7. Grau, B.C., Horrocks, I., Kazakov, Y., Sattler, U.: Just the right amount: Extract- ing modules from ontologies. In: Proceedings of the 16th International Conference on World Wide Web. pp. 717–726. WWW ’07, ACM, New York, NY, USA (2007), http://doi.acm.org/10.1145/1242572.1242669 8. Horridge, M., Parsia, B., Sattler, U.: Justification masking in ontologies. In: Brewka, G., Eiter, T., McIlraith, S.A. (eds.) Proc. of the 12th Int. Conf. on the Prin- ciples of Knowledge Representation and Reasoning (KR-12). AAAI Press (2012) 9. Jabbour, S., Ma, Y., Raddaoui, B.: Inconsistency measurement thanks to mus decomposition. In: International conference on Autonomous Agents and Multi- Agent Systems (AAMAS’14) (2014), to appear 10. Jiménez-Ruiz, E., Grau, B.C., Zhou, Y., Horrocks, I.: Large-scale interactive on- tology matching: Algorithms and implementation. In: Raedt, L.D., Bessière, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P.J.F. (eds.) Proc. of the 20th European Conf. on Artificial Intelligence (ECAI-12). Frontiers in Artificial Intelligence and Applications, vol. 242, pp. 444–449. IOS Press (2012) 11. Kalyanpur, A.: Debugging and Repair of OWL Ontologies. Ph.D. thesis, The Grad- uate School of the University of Maryland (2006) 12. Kalyanpur, A., Parsia, B., Sirin, E., Hendler, J.A.: Debugging unsatisfiable classes in owl ontologies. J. Web Sem. 3(4), 268–293 (2005) 13. Lembo, D., Lenzerini, M., Rosati, R., Ruzzi, M., Savo, D.F.: Inconsistency-tolerant semantics for description logics. In: Hitzler, P., Lukasiewicz, T. (eds.) Proc. of the 4th Int. Conf. on Web Reasoning and Rule Systems (RR’10). Lecture Notes in Computer Science, vol. 6333, pp. 103–117. Springer (2010) 14. Ma, Y., Peñaloza, R.: Towards parallel ontology repair using decompositions. LTCS-Report 14-05, Chair for Automata Theory, Institute for Theoretical Com- puter Science, Technische Universität Dresden, Dresden, Germany (2014), see http://lat.inf.tu-dresden.de/research/reports.html. 15. Meilicke, C.: Alignment incoherence in ontology matching. Ph.D. thesis, University of Mannheim, Chair of Artificial Intelligence (2011) 16. Peñaloza, R., Sertkaya, B.: On the complexity of axiom pinpointing in the el family of description logics. In: Lin, F., Sattler, U., Truszczynski, M. (eds.) Proc. of the 12th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR-10). AAAI Press (2010) 17. Peñaloza, R.: Axiom Pinpointing in Description Logics and Beyond. Ph.D. the- sis, Institute for Theoretical Computer Science, Faculty of Computer Science, TU Dresden, Germany (2009) 18. Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (Apr 1987), http://dx.doi.org/10.1016/0004-3702(87)90062-2 19. Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence. pp. 355–360. Morgan Kaufmann Publishers Inc. (2003), http://dl.acm.org/citation.cfm?id=1630659.1630712 20. Suntisrivaraporn, B.: Polynomial-Time Reasoning Support for Design and Mainte- nance of Large-Scale Biomedical Ontologies. Ph.D. thesis, Institute for Theoretical Computer Science, Faculty of Computer Science, TU Dresden, Germany (2009)