Debugging EL Ontologies through Horn MUS Enumeration

Abstract

In description logics (DLs), axiom pinpointing refers to the problem of enumerating the minimal subsets of axioms from an ontology that entail a given consequence. Recent developments on axiom pinpointing for the light-weight DL EL+ are based on translating this problem into the enumeration of all minimally unsatis able subformulas (MUSes) of a propositional formula, and using advanced SAT-based techniques for solving it. Further optimizations have been obtained by targeting the MUS enumerator to the speci c properties of the formula obtained. In this paper we describe di erent improvements that have been considered since the translation was rst proposed. Through an empirical study, we analyse the behaviour of these techniques and how it depends on di erent characteristics of the original pinpointing problem, and the translated SAT formula.

Introduction

Description logics, in particular those from the EL family, have been successfully used to represent the knowledge of many application domains, forming large ontologies. And their popularity is continuously increasing. Ontology development, however, is very error-prone and it is not uncommon to nd unwanted (or unexpected) consequences being entailed. To understand and correct the causes of these consequences on existing ontologies|some of which have hundreds of thousands of axioms|without the help of any automated tools would be impossible. Axiom pinpointing refers to the task of nding the precise axioms in an ontology that cause a consequence to follow [ 28 ], or that need to be corrected for avoiding it.

Recent years have witnessed remarkable improvements in axiom pinpointing technologies, specially for logics in the EL family [2, 3, 6{8, 22, 23, 36, 37]. Among these, the use of SAT-based methods [ 2,3,36 ] has been shown to outperform other alternative approaches very signi cantly. These methods reduce the axiom pinpointing problem to a propositional Horn formula, and apply highly-optimized SAT tools, along with some ad-hoc optimizations to enumerate all the (minimal) subontologies that entail the consequence. Recently, it was shown that the use of techniques developed speci cally to handle Horn formulas can further improve the performance of these methods [ 1 ].

In this paper, we propose an integrated tool for analysing ontologies that integrates di erent methods for solving axiom pinpointing and other related problems. Speci cally, we show that by considering the shape of the Horn formula obtained, we can explain and repair consequences from ontologies, and also nd justi cations of a desired size, among other tasks. An experimental analysis shows the behaviour of these techniques, and how it depends on the characteristics of the input problem, and in particular of the output it produces. 2

Preliminaries

We assume some basic knowledge of the DL EL+ [ 5 ] and propositional logic [ 10 ], but we brie y recall the main notions needed for this paper. 2.1

The Lightweight Description Logic EL+ In the DL EL+, concepts are built from two disjoint sets NC and NR of concept names and role names through the grammar rule C ::= A j > j C u C j 9r:C, where A 2 NC and r 2 NR. The knowledge of the domain is stored in a TBox : a nite set of general concept inclusions (GCIs) of the form C v D, where C and D are EL+ concepts, and role inclusions (RIs) of the form r1 rn v s, where n 1 and ri; s 2 NR. We will often use the term axiom to refer to both GCIs and RIs.

The semantics of this logic is based on interpretations, which are pairs of the form I = ( I ; I ) where I is a non-empty set called the domain and I is the interpretation function that maps every A 2 NC to a set AI I and every r 2 NR to a binary relation rI I I . The interpretation I satis es the GCI C v D i CI DI ; it satis es the RI r1 rn v s i r1I rnI sI , where denotes the composition of binary relations. I is a model of T i I satis es all its GCIs and RIs.

The main reasoning problem in EL+ is to decide subsumption between concepts. A concept C is subsumed by D w.r.t. T (denoted C vT D) if for every model I of T it holds that CI DI . Classi cation refers to the task of deciding all the subsumption relations between concept names appearing in T . Rather than merely deciding whether a subsumption relation follows from a TBox, we are interested in understanding the causes of this consequence, and repairing it if necessary.

C 6vT n D D.4 De nition 1 (MinA, diagnosis). A MinA for C v D w.r.t. the TBox T is a minimal subset (w.r.t. set inclusion) M T such that C vM D. A diagnosis for C v D w.r.t. T is a minimal subset (w.r.t. set inclusion) D T such that It is well known that MinAs and diagnoses are closely related by minimal hitting set duality [ 21,35 ]. More precisely, the minimal hitting sets of the set of all MinAs is exactly the set of all repairs, and vice versa. 4 MinAs are also often called justi cations in the literature [ 17, 34 ].

Example 2. Consider the TBox Texa = fA v 9r:A; A v Y; 9r:Y v B; Y v Bg. There are two MinAs for A v B w.r.t. Texa, namely M1 = fA v Y; Y v Bg, and M2 = fA v 9r:A; A v Y; 9r:Y v Bg. The diagnoses for this subsumption relation are fA v Y g, fA v 9r:A; Y v Bg, and f9r:Y v B; Y v Bg. 2.2

Propositional Satis ability

In propositional logic, we consider a set of Boolean (or propositional) variables X. A literal is either a variable x 2 X or its negation (:x). The former are called positive literals, and the latter are negative. A nite disjunction of literals is called a clause. Finally, a CNF formula (or formula for short) is a nite conjunction of clauses. One special class of formulas are Horn formulas. These are CNF formulas whose clauses contain at most one positive literal.

Clauses and formulas are interpreted via truth assignments. A truth assignment is a mapping : X ! f0; 1g. This truth assignment is extended to literals, clauses, and formulas in the obvious manner. If satis es the formula F , then is called a model of F . Propositional satis ability refers to the problem of deciding whether a given formula F has a model or not. If it does not have a model, then F is called unsatis able. As it is well known, this problem is in general NP-complete. However, when considering only Horn formulas, satis ability is decidable in polynomial time [ 13, 16, 27 ].

Just as in the case of description logics, one is sometimes interested in understanding (and correcting) the causes for unsatis ability of a formula. For this reason, the following subsets are usually considered [ 21, 25 ].

De nition 3 (MUS, MCS). Let F be an unsatis able formula. A subformula M F is called minimally unsatis able subset (MUS) of F i M is unsatis able and for all c 2 M; M n fcg is satis able. The formula C F is a minimal correction subset (MCS) i F n C is satis able and for all c 2 C; F n (C n fcg) is unsatis able.

MUSes and MCSes are related by hitting set duality [ 9, 11, 32, 39 ]. Notice that MUSes and MCSes are closely related to MinAs and diagnoses from De nition 1, respectively. Indeed, although EL+ and propositional logic di er in expressivity and in the inferences of interest, in both cases the goal is to nd minimal information that explains, or removes, the inference.

A generalization of the notion of a MUS is that of a group-MUS [ 21 ]. In this case, the clauses of the unsatis able formula F are partitioned into groups, and the goal is not to nd the speci c clauses that cause unsatis ability, but the groups to which they belong. This notion is formalized next.

De nition 4 (Group-MUS). Given an explicitly partitioned unsatis able CNF formula F = G0 [ ::: [ Gk, a group-MUS of F is a set of groups G fG1; :::; Gkg, such that G0 [ SGi2G Gi is unsatis able, and for every Gj 2 G, G0 [ SGi2G;i6=j Gi is satis able.

Notice that MUSes are a special cases of group-MUSes in which the group G0 is empty, and all other groups are singletons, containing a clauses from F . One can also de ne the generalization of MCSes to group-MCSes in the obvious way. In the following, we will often call a formula whose clauses have been partitioned in groups as in De nition 4 a group formula.

During the last years, highly-optimized methods for the enumeration of (group-)MUSes of propositional formulas have been developed and implemented. Taking advantage of these developments, it has been proposed to translate the problem of enumerating MinAs and diagnoses in DLs|and in particular in EL+|to MUS and MCS enumeration in propositional logic. In the following section we brie y recall the basic ideas of this translation and present a few further insights for improving the overall e ciency of MinA enumeration. 3

The SAT Encoding

The main problem we consider in this section is the enumeration of the MinAs and diagnoses for a given subsumption relation w.r.t. an EL+ TBox T . Our approach consists of three main components: The rst one classi es the TBox T and encodes the classi cation procedure into a set of Horn clauses H. Given a subsumption relation entailed by T , which we aim to analyze, the second component creates and simpli es an unsatis able Horn formula, and partitions it in a suitable manner to reduce the DL enumeration problems into group-MUS and group-MCS enumerations. Finally, the third component computes groupMUSes and group-MCSes, corresponding to MinAs and diagnoses, respectively. Each of its components is explained in more detail next. 3.1

Classi cation and Horn Encoding

During the classi cation of T , a Horn formula H is created according to the method introduced in EL+SAT [ 36, 37 ]. To this end, each axiom ai 2 T is initially assigned a unique selector variable s[ai]. The classi cation of T is done in two phases (see [ 5, 7 ] for more details).

First, T is normalized so that it only contains GCIs of the forms (A1 u ::: u Ak) v B

A v 9r:B 9r:A v B; where A; Ai; B 2 NC [f>g and k

1, and RIs of the form

r1 ::: rn v s with r; ri; s 2 NR and n 1. The normalization process runs in linear time and results in a TBox T N where each axiom ai 2 T is substituted by a set of axioms in normal form fai1; :::; aimi g. At this point, the clauses s[ai] ! s[aik], with 1 k mi, are added to the Horn formula H.

Then, the normalized TBox T N is saturated through the exhaustive application of the completion rules shown in Table 1, resulting in the extended TBox T 0. Each of the rows in Table 1 constitute a so-called completion rule. Their application is sound and complete for inferring (atomic) subsumptions [ 5 ]. Whenever a rule r can be applied (with antecedents ant(r)) leading to inferring an axiom ai, the Horn clause (Vfaj2ant(r)g s[aj]) ! s[ai] is added to H.

The completion algorithm|and hence the construction of the formula H| terminates after polynomially many rule applications. The result of this construction is a Horn formula that encodes all possible derivations that can be obtained through applications of the completion algorithm, to infer any atomic subsumption relation; that is, any entailment X vT Y , with X; Y 2 NC. After classifying T , the extended TBox T 0 contains all atomic subsumptions that can be derived from T . For a given such entailment A v B 2 T 0, we might be interested in computing their MinAs or diagnoses. Each of these queries will result in a group Horn formula de ned as: HG = fG0; G1; :::; Gj T jg, where G0 = H [ f(:s[AvB])g and for each axiom ai (i > 0) in the original TBox T , the group Gi = f(s[ai])g is de ned with a single unit clause de ned by the selector variable of the axiom. By construction, HG is unsatis able. Moreover, its group-MUSes correspond to the MinAs for A vT B (see [ 2,3 ] for the full details). Equivalently, due to the hitting set duality between MinAs and diagnoses, which also holds for group-MUSes and group-MCSes, the group-MCSes of HG correspond to the diagnoses for A vT B.

To improve the e ciency of these enumeration problems, the formula HG is often simpli ed through di erent techniques. In particular, two simpli cation techniques based on syntactic modularization were proposed in [ 36, 37 ]. These techniques have been shown to reduce the size of the formulas to a great extent. The last step in the process is to enumerate all the group-MUSes or group-MCSes of the formula HG constructed in Section 3.2. Previous work has proposed the use of a general purpose MUS enumerator, or other techniques focused on propositional formulas, together with some ad-hoc optimizations [ 23, 24, 36, 37 ]. In contrast, we exploit the fact that HG is a Horn formula, which can be treated

Algorithm 1: eMUS [30] / MARCO [20]

Input: F a CNF formula

Output: Reports the set of MUSes (and MCSes) of F 1 hI; Qi hfpi j ci 2 F g; ;i 2 while true do 3 (st; P ) MaximalModel(Q) 4 if not st then return 5 F 0 fci j pi 2 P g 6 if not SAT(F 0) then 7 M ComputeMUS(F 0) 8 ReportMUS(M) 9 b f:pi j ci 2 Mg 10 else 11 12

ReportMCS(F n F 0) b fpi j pi 2 I n P g 13

Q

Q [ fbg // Variable pi picks clause ci

// Pick selected clauses // Negative clause blocking the MUS // Positive clause blocking the MCS more e ciently via optimized unit propagation techniques. Thus, we enumerate group-MUSes and group-MCSes using the state-of-the-art HgMUS enumerator [ 3 ]. HgMUS exploits hitting set dualization between (group-) MCSes and (group-) MUSes and, hence, it shares ideas also explored in MaxHS [ 12 ], EMUS/MARCO [ 19, 30 ], and many other systems.

As shown in Algorithm 1, these methods rely on a two (SAT) solvers approach. The formula Q is de ned over a set of selector variables corresponding to the clauses in F . This formula is used to enumerate subsets of F . Iteratively, the algorithm computes a maximal model P of Q and tests whether the subformula F 0 F containing the clauses associated to P is satis able. If this formula is satis able, then F n F 0 is an MCS of F . Otherwise, F 0 can be reduced to an MUS, and the result of this reduction is reported. To avoid observing the same MUS or MCS in a later iteration, all such sets found are blocked by adding the respective clauses to Q.

HgMUS shares the main organization of Algorithm 1, with F = G0 and Q de ned over selector variables for groups Gi of HG, with i > 0. However, it also includes some speci c features for handling Horn formulas more e ciently. First, it uses linear time unit resolution (LTUR) [ 27 ] to check satis ability of the formula in linear time. Additionally, HgMUS integrates a dedicated insertionbased MUS extractor as well as an e cient algorithm for computing maximal models. The latter is based on a recently proposed reduction from maximal model computation to MCSes computation [ 26 ]. 3.4

Additional Features

Although the main goal of this work is to enumerate the MinAs and diagnoses of a given consequence, it is important to notice that the construction of the Horn formula HG described earlier in this section can be used, together with other advanced techniques from propositional satis ability, to provide additional services to axiom pinpointing. We describe some of these next.

Diagnosing Multiple Subsumption Relations Simultaneously De ni

tion 1 considers only one subsumption relation that needs to be understood or removed. However, in a typical knowledge engineering work ow one will often be interested in looking at several consequences simultaneously. For example, if several errors are detected, then one wants to nd a maximal subset of the TBox that does not imply any of those errors. Once that the formula HG is constructed, it is possible to look at several atomic subsumptions as follows. Given a set of atomic subsumptions Ai v Bi 2 T 0, 1 i n, one needs simply to add all the unit clauses (:s[AivBi]) to G0 in HG. In this case, the formula becomes unsatis able as soon as any of the atomic subsumptions is derivable. Thus, a group-MCS for this formula corresponds to a diagnosis that eliminates all these subsumption relations. Analogously, a group-MUS corresponds to axioms that entail at least one of these consequences.

Computing Smallest MinAs Alternatively to enumerating all the possible MinAs, one may want to compute only those of the minimum possible size. This would be the case, for instance, when the MinA will be reviewed by a human expert, and retrieving large subsets of the TBox T would make the task of understanding them harder. To enable this functionality, one can simply integrate a state-of-the-art solver for the smallest MUS (SMUS) problem such as Forqes [ 15 ]. Notice that the decision version of the SMUS problem is known to be 2p-complete for general CNF formulas [ 14, 18 ], but this complexity bound is lowered to NP-completeness for Horn formulas [ 7, 28 ]. As HgMUS, Forqes is based on the hitting set dualization between (group) MUSes and (group) MCSes. The tool iteratively computes minimum hitting sets of a set of MCSes of a formula detected so far. While these minimum hitting sets are satis able, they are grown into a maximal satis able subformula (MSS), whose complement is an MCS which is added to the set of MCSes. The process terminates when an unsatis able minimum hitting set is identi ed, representing a smallest MUS of the formula.

All these features have been implemented in the system BEACON [ 1 ], which is available at http://logos.ucd.ie/web/doku.php?id=beacon-tool. The performance of this system has been analyzed, in comparison to other existing axiom pinpointing tools, in previous work [ 1 ]. In the following section we perform an empirical analysis aiming at understanding the behaviour of BEACON in relation to di erent characteristics of the input problem and the propositional formula obtained. In this section, we present some experimental results aimed to understanding the properties of our approach and its behaviour on di erent kinds of instances. To this end, we took the instances originally proposed by Sebastiani and Vescovi [ 37 ], which have become de facto benchmarks for axiom pinpointing tools in EL+. The experimental setup considers 500 subsumption relations that follow from ve well-known EL+ bio-medical ontologies. These are GALEN [ 31 ] (FULL-GALEN and NOT-GALEN), the Gene Ontology (GO) [ 4 ], NCI [ 38 ], and SNOMED-CT [ 40 ]. Speci cally, for each of these ontologies, 100 subusmption relations were chosen: 50 were randomly selected from the space of all entailed subsumption relations, and 50 were selected as those that appear most often in the head of a Horn clause in the encoding. This choice was made as a heuristic for instances that should contain more MinAs and be harder to solve (see [ 37 ]) for the full details.

For each of these 500 instances, we considered three variants: the full formula, as obtained through the construction described in Section 3, and the smaller formulas obtained after applying the cone of in uence (COI) and x2 optimizations from [ 37 ]. Intuitively, the COI technique traverses the formula backwards, considering the clauses containing assertions that were used for deriving the queried subsumption relation. The COI module consists of the set of (original) axioms that were found in the computation of the COI formula. The x2 technique encodes the subontology represented by the COI module, which usually results in a smaller Horn formula, containing the same axiom variables. Overall, this gives us a corpus of 1500 Horn formulas of varying size and structure, and providing a large range of hardness (see Table 2). For our experiments, all these formulas were fed to the back-end engine used by BEACON; that is, to HgMUS. The experiments were run on a Linux cluster (2Ghz) with a time limit of 3600s and 4Gbytes of memory.

3 0 + e 1 1e+02 1e+04 #Clauses 1e+06 1e+08

As explained before, our goal is not to compare the performance of HgMUS against other proposed approaches. Such a comparison can be found in previous work [ 1, 3 ]. Likewise, the e ect of the two proposed optimizations (COI and x2) has been analysed in detail in [ 37 ] (albeit, in a di erent system). One conclusion obtained from the latter analysis is that the COI optimization improves the results over the full formula, and x2 performs better than COI.

A simple analysis shows that the same behaviour is observed when HgMUS is used as the underlying Horn MUS enumeration tool. One possible explanation for the improvements obtained through COI and x2 is that these optimizations produce smaller formulas with smaller axioms, which are easier to handle by HgMUS. Recall, in addition, that ontology size is a very good predictor for hardness of inferences in DLs [ 33 ]. Through Figure 1, we observe that this intuition is correct, but there are other factors in uencing the performance of the enumerator. The gure compares the time required to solve an instance (y-axis) against the size of the formula and number of axioms used in that instance (shown in the gradient). While it is true that time tends to increase as either of these factors grows, the correlation is not very high. See for example the cluster of instances with over 50,000 clauses and 1000 axioms that are solved in no time (bottom line of the gure).

A better predictor for the time needed to nd all MinAs seems to be the size of the output. As seen in Figure 2, the time required to solve an instance increases with both, the number of MinAs found in that instance (shown through the gradient, where a colder color means a larger number of MinAs), and the average size of the MinAs found (shown through the size of the dots in the plot). Notice that there is a large concentration of big, cold dots at the top line of the 3 0 + e 1 Avg. MinA size 1e+02 #Clauses 1e+05 1e+08 plot. Some of these correspond to the 73 instances that timed-out. Interestingly, in one instance we were able to enumerate over 3200 MinAs before the allocated time of 3600s. was spent. For comparison, notice that the average number of MinAs found over all the instances is below 20, and when restricted to only those instances fully solved, this average drops down to 6.5.

Finally, we verify whether the theoretical output-complexity hardness of MinA enumeration is observed also in practice. In a nutshell, it is known that as more MinAs are found, it becomes harder to nd a new one, or to decide whether no additional solutions exist [ 29 ]. As shown in Figure 3, the maximum delay between solutions increases with the number of MinAs. However, the relation to the average delay is not so direct.

In order to understand these relationships in more detail, we will need to design experiments aimed at nding the di erentiating properties of the hard and simple instances observed. In addition, we will need to develop better optimizations that will allow us to fully solve the missing instances, at least over the reduced formulas. Both of these steps will be the focus of future work. 5

Conclusions

In this paper, we have presented a new approach for enumerating MinAs in the light-weight DL EL+ through the enumeration of Horn group-MUSes. The approach is based on a previously explored translation from EL+ to Horn formulas. One of the di erentiating features of our proposal is that it uses a dedicated Horn enumeration tool, which is able to exploit the linear time unit resolution algorithm available for this logic.

0 0 1 ()s 75 y a l e D aeg 50 r e v A 5 2 0 10 #MinAs 1000

By using the properties of propositional Horn formulas, we show that it is possible not only to e ciently enumerate all MinAs for large EL+ ontologies, but also solve other associated problems, like repairing an error, or nding justi cations of minimal size. Interestingly, the e ectiveness of our methods depends only on the existence of a Horn formula, and not on the properties of EL+; thus, it should be possible to produce e cient axiom pinpointing and repair methods for other DLs as well.

Through an empirical evaluation, we observe that the size of the output is an important contributing factor to the total time spent by our method. Since we cannot avoid generating this output, it is unclear how our methods can be improved to avoid such a bottleneck. However, we plan to further analyse the behaviour of the MinA enumeration, and extend it with an analysis of the other related reasoning tasks, to identify potential improvements, or cases that can be solved easily.

References

1. M. F. Arif , C. Menc a, A . Ignatiev, N. Manthey , R. Pen ~aloza, and J. MarquesSilva. BEACON: an e cient sat-based tool for debugging EL+ ontologies . In N. Creignou and D. L . Berre, editors, Proceedings of the 19th International Conference on Theory and Applications of Satis ability Testing (SAT 2016 ), volume 9710 of Lecture Notes in Computer Science, pages 521 { 530 . Springer, 2016 .

2. M. F. Arif , C. Menc a, and J. Marques-Silva . E cient axiom pinpointing with EL2MCS . In KI , pages 225 { 233 , 2015 .

3. M. F. Arif , C. Menc a, and J. Marques-Silva . E cient MUS enumeration of Horn formulae with applications to axiom pinpointing . In SAT , pages 324 { 342 , 2015 .

4. M. Ashburner , C. A. Ball , J. A. Blake , D. Botstein , H. Butler , J. M. Cherry , A. P. Davis , K. Dolinski , S. S. Dwight , J. T. Eppig , and et al. Gene ontology: tool for the uni cation of biology . Nat. Genet ., 25 ( 1 ): 25 { 29 , 2000 .

5. F. Baader , S. Brandt , and C. Lutz . Pushing the EL envelope . In IJCAI , pages 364 { 369 , 2005 .

6. F. Baader , C. Lutz , and B. Suntisrivaraporn. CEL - A polynomial-time reasoner for life science ontologies . In IJCAR , pages 287 { 291 , 2006 .

7. F. Baader , R. Pen~aloza, and B. Suntisrivaraporn . Pinpointing in the description logic EL+ . In KI , pages 52 { 67 , 2007 .

8. F. Baader and B. Suntisrivaraporn . Debugging SNOMED CT using axiom pinpointing in the description logic EL+ . In KR-MED , 2008 .

9. J. Bailey and P. J. Stuckey . Discovery of minimal unsatis able subsets of constraints using hitting set dualization . In PADL , pages 174 { 186 , 2005 .

10. A. Biere , M. Heule , H. van Maaren , and T. Walsh, editors. Handbook of Satis ability , volume 185 of Frontiers in Arti cial Intelligence and Applications . IOS Press, 2009 .

11. E. Birnbaum and E. L. Lozinskii . Consistent subsets of inconsistent systems: structure and behaviour . J. Exp. Theor. Artif. Intell. , 15 ( 1 ): 25 { 46 , 2003 .

12. J. Davies and F. Bacchus . Solving MAXSAT by solving a sequence of simpler SAT instances . In CP , pages 225 { 239 , 2011 .

13. W. F. Dowling and J. H. Gallier . Linear-time algorithms for testing the satis ability of propositional Horn formulae . J. Log. Program. , 1 ( 3 ): 267 { 284 , 1984 .

14. A. Gupta . Learning Abstractions for Model Checking . PhD thesis , Carnegie Mellon University, June 2006 .

15. A. Ignatiev , A. Previti , M. Li ton, and J. Marques-Silva . Smallest MUS extraction with minimal hitting set dualization . In CP , 2015 .

16. A. Itai and J. A. Makowsky . Uni cation as a complexity measure for logic programming . J. Log. Program. , 4 ( 2 ): 105 { 117 , 1987 .

17. A. Kalyanpur , B. Parsia , M. Horridge , and E. Sirin . Finding all justi cations of OWL DL entailments . In ISWC , pages 267 { 280 , 2007 .

18. P. Liberatore . Redundancy in logic I: CNF propositional formulae . Artif . Intell., 163 ( 2 ): 203 { 232 , 2005 .

19. M. H . Li ton and A. Malik . Enumerating infeasibility: Finding multiple MUSes quickly . In CPAIOR , pages 160 { 175 , 2013 .

20. M. H. Li ton , A. Previti , A. Malik , and J. Marques-Silva . Fast, exible MUs enumeration . Constraints , 2015 . Online version: http://link.springer.com/ article/10.1007/s10601-015-9183-0.

21. M. H . Li ton and K. A . Sakallah . Algorithms for computing minimal unsatis able subsets of constraints . J. Autom. Reasoning , 40 ( 1 ):1{ 33 , 2008 .

22. M. Ludwig . Just: a tool for computing justi cations w .r.t. ELH ontologies. In ORE , 2014 .

23. N. Manthey and R. Pen ~aloza. Exploiting SAT technology for axiom pinpointing . Technical Report LTCS 15-05 , Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universitat Dresden, April 2015 . Available from https://ddll.inf.tu-dresden.de/web/Techreport3010.

24. N. Manthey , R. Pen ~aloza, and S. Rudolph . E cient axiom pinpointing in EL using SAT technology . In M. Lenzerini and R. Pen~aloza, editors, Proceedings of the 29th International Workshop on Description Logics, (DL 2016 ), volume 1577 of CEUR Workshop Proceedings. CEUR-WS.org , 2016 .

25. J. Marques-Silva , F. Heras , M. Janota , A. Previti , and A. Belov . On computing minimal correction subsets . In IJCAI , pages 615 { 622 , 2013 .

26. C. Menc a, A. Previti, and J. Marques-Silva . Literal-based MCS extraction . In IJCAI , pages 1973 { 1979 , 2015 .

27. M. Minoux . LTUR: A simpli ed linear-time unit resolution algorithm for Horn formulae and computer implementation . Inf. Process. Lett., 29 ( 1 ):1{ 12 , 1988 .

28. R. Pen ~aloza. Axiom pinpointing in description logics and beyond . PhD thesis , Dresden University of Technology, 2009 .

29. R. Pen~aloza and B. Sertkaya . On the complexity of axiom pinpointing in the EL family of description logics . In KR , 2010 .

30. A. Previti and J. Marques-Silva . Partial MUS enumeration . In AAAI , pages 818 { 825 , 2013 .

31. A. L. Rector and I. R. Horrocks . Experience building a large, re-usable medical ontology using a description logic with transitivity and concept inclusions . In Workshop on Ontological Engineering , pages 414 { 418 , 1997 .

32. R. Reiter . A theory of diagnosis from rst principles . Artif . Intell., 32 ( 1 ): 57 { 95 , 1987 .

33. V. Sazonau , U. Sattler , and G. Brown. Predicting performance of OWL reasoners: Locally or globally ? In C. Baral, G. D. Giacomo , and T. Eiter, editors, Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning (KR 2014 ). AAAI Press, 2014 .

34. S. Schlobach and R. Cornet . Non-standard reasoning services for the debugging of description logic terminologies . pages 355 { 362 . Morgan Kaufmann, 2003 .

35. S. Schlobach and R. Cornet . Non-standard reasoning services for the debugging of description logic terminologies . In IJCAI , pages 355 { 362 , 2003 .

36. R. Sebastiani and M. Vescovi . Axiom pinpointing in lightweight description logics via Horn-SAT encoding and con ict analysis . In CADE , pages 84 { 99 , 2009 .

37. R. Sebastiani and M. Vescovi . Axiom pinpointing in large EL+ ontologies via SAT and SMT techniques . Technical Report DISI-15-010 , DISI, University of Trento, Italy, April 2015 . Under Journal Submission . Available as http://disi.unitn. it/~rseba/elsat/elsat_techrep.pdf.

38. N. Sioutos , S. de Coronado, M. W. Haber , F. W. Hartel , W. Shaiu , and L. W. Wright . NCI thesaurus: A semantic model integrating cancer-related clinical and molecular information . J. Biomed . Inform., 40 ( 1 ): 30 { 43 , 2007 .

39. J. Slaney . Set-theoretic duality: A fundamental feature of combinatorial optimisation . In ECAI , pages 843 { 848 , 2014 .

40. K. A. Spackman , K. E. Campbell, and R. A. Co ^te. SNOMED RT: a reference terminology for health care . In AMIA , 1997 .