Over the past few years there has been a signi cant amount of interest in the area of debugging and repairing of OWL ontologies. The process of debugging an ontology is necessary in the same way that debugging programme code is necessary { that is, debugging takes place in order to eradicate faults. In terms of ontology debugging, the faults manifest themselves as undesirable entailments. In particular, the entailment that a concept is unsatis able is almost always undesired. However, undesirable entailments are not restricted to unsatis able concepts. Other entailments, such as certain subsumptions between concepts, might be unintended and contrary to the modeler's understanding of the domain, and thus, undesirable. Ontology debugging is the process of nding the causes of an undesirable entailment, understanding these causes, and modifying the ontology so that the undesirable entailment no longer holds. Without some kind of tool support, it can be very di cult, or even impossible, to work out why entailments arise in ontologies. Even in small ontologies, that only contain tens of axioms, there can be multiple reasons for an entailment, none of which may be obvious. It is for this reason that there has recently been a lot of focus on generating explanations for entailments in ontologies. In the OWL world, justi cations are a popular form of explanation for entailments. Justi cations are minimal subsets of an ontology that are su cient for an entailment to hold. Virtually all mainstream ontology editors such as Protege-4, Swoop, and Top Braid Composer provide support for generating justi cations as explanations for arbitrary entailments. Justi cations have proved enormously useful for understanding and debugging ontologies. In [1], Kalyanpur presents a user study which showed that the availability of justi cations had a signi cant positive impact on the ability of users to successfully diagnose and repair an ontology. Recently, justi cations have been used for debugging very large ontologies such as SNOMED [2], where the size of the ontology prohibits e cient manual debugging. In the same way that debugging software requires an understanding of why errors in the code occur, it is necessary to understand why undesirable or unexpected entailments arise in a buggy ontology. Without this understanding, it ? The user studies that form part of this work were approved by the University of Manchester Senate Ethics Committee. Reference 0723
is essentially impossible to devise any kind of reasonable repair strategy for an ontology. However, people can nd it di cult to understand certain justi cations. Indeed, as will be seen later, there is evidence that some justi cations are very di cult, or even impossible, for a wide range of people to understand. The ability to understand a justi cation is a ected by many factors ranging from presentation techniques through to the interplay between the various types of axioms in the justi cation. This paper focuses on the latter aspect. The work presented in this paper focuses on taking justi cations that are di cult to understand, and choosing subsets of these justi cations that can be replaced with simpler summarising entailments, such that the result is an easier to understand justi cation. Note that it is highly unlikely that this service should be directly exposed to end users. Instead, it is envisioned that a debugging tool will make multiple calls to this service in order to build proof structures to present to users. 2
Throughout this paper, the following nomenclature is used:
an axiom O an ontology
an entailment J a justi cation SS? tahseetdsedoufcatxivioemcslosure of S Sig(X) the signature of X
A and B are used as atomic concept names, C, D, E are used as (possibly
complex) concepts, R and S as role names. This paper focuses on OWL and
OWL 2 and their rough syntactic variants SHOIN (D) [
Consider the following ontology, O = f1 : A v B; 2 : A v 9R:A; 3 : D 9R:B; 4 : A v F; 5 : B v Dg which entails A v D. There are two justi cations for A v D, the rst being f1; 2; 3g and the second being f1; 5g. Notice that if any one of the axioms is removed from any of these justi cations, then the remaining set of axioms no longer supports the entailment. 3
Through personal experience and through the observation of users working with justi cations, the intuition that some justi cations can be very di cult or even impossible for people to understand has emerged. In order to verify this intuition, we conducted a user study. The aim of the study was to gather su cient data on the di culty of understanding justi cations in order to develop, calibrate, and validate a model for predicting how easy or di cult it would be for people to understand a given justi cation. 3.1
Participants Generally speaking, people who view justi cations of entailments do so within the context of an ontology development environment. Users request justi cations for entailments during the editing or browsing process when they encounter undesirable entailments or entailments that they do not understand. The target population of the study was therefore people who have had experience of either browsing, editing, or using OWL ontologies. The target population did not include OWL neophytes, or people with a very limited understanding of OWL who would nd it di cult to read and interpret OWL axioms. Given the target population, it was reasonable for the study sample to comprise sta and students from computer science departments, Semantic Web researchers, and people from other research communities who are familiar with OWL. Procedure We collected a corpus of justi cations for entailments found in published OWL ontologies. The entailments were either unsatis able concept entailments (A ?) or subsumption entailments between named concepts (A v B). We selected a subset of the corpus which seemed di cult for people to understand (e.g., we removed trivial justi cations such as those consisting of the entailment itself). We then expanded the set of justi cations using various substitution lemmas that we speculated would make justi cations easier to understand. In total this provided a pool of 100 justi cations which were used in the study. In order to remove biasing e ects from domain knowledge (or lack of domain knowledge), justi cations were obfuscated by replacing the names of entities with alpha-numeric identi ers.
A random selection of justi cations was presented to each participant. For each justi cation, we recorded the time taken for the participant to claim that they had understood (or had not understood) the justi cation. The \think aloud protocol" was used in order for the study facilitator to determine whether or not the participant had, in fact, understood the justi cation. We also recorded the participant's ranking on how easy or di cult the justi cation was to understand using a six point Likert scale: f`Very easy'=1, `Easy'=2, `Neither easy or di cult'=3, `Di cult'=4, `Very di cult'=5, `Impossible'=6g.
Results A total of 12 people participated in the study. The participants' experience with OWL ranged from less than 6 months to over 4 years. Some participants only had experience in browsing ontologies, while other participants develop OWL tools. The total number of rankings, a ranking being an instance of a viewing of a justi cation, was 227 (an average of 18.9 rankings per participant). Figure 1 shows a plot of ranking versus time (in seconds). Each point represents a ranking. A rank of 1 corresponds to \very easy to understand", and a rank of 6 corresponds to \impossible to understand". Excluding ranking 6 (\impossible to understand") the general trend indicates that when participants took longer to understand a justi cation they perceived it to be more di cult to understand. It is noticeable that, in many cases the time spent trying to understand justi cations that were deemed impossible to understand (raking 6), is less than the time spent trying to understand very di cult justi cations. This indicates that participants gave up trying to understand a justi cation very soon, perhaps because it simply seemed to complicated, or, after some e ort they thought that they would never understand the justi cation. In fact, it was common for participants who could not understand a particular justi cation to ask the question, \Is this explanation correct?", thereby implying that they doubted the ability of the system to generate sound justi cations. Out of the 227 rankings, 69 (30%) corresponded to being \di cult to understand" through to \impossible to understand" (35 rankings, (15%) corresponded to being \impossible" to understand). Interestingly, all of the \impossible to understand" rankings were rankings of unmodi ed, naturally occurring, justi cations. In summary, there were a significant number of \di cult" to \impossible" to understand justi cations, which indicates that understanding justi cations is a real problem. 3.2
Data from the user study provided insight into how people understand justi cations and why they nd certain justi cations di cult to understand. Broadly speaking, the following reasons were identi ed as being important.
When people work through justi cations they typically perform obvious syntactic transformation of axioms and spot simple patterns to reach intermediate conclusions. For example, a user might work through a justi cation, such as f1; 2; 3g, from the Example in Section 2, as follows: Axioms 1 and 2 entail A v 9R:B, and this result, in conjunction with Axiom 3 entails A v D (the entailment). Note that the user must spot a suitable intermediate inference step, understand how it arises, and understand the part it plays in the whole justi cation. Justi cations that contain a lot of information, and a lot of intermediate inference steps, are di cult to understand. In particular, the number of di erent types of axioms and concept expressions that the justi cation contains plays an '$!!" '#!!" %,'!!!" ' + *)&!!" '($ %&$ %!!" "!#$!!" #!!" !" 200 180 g160 iknn140 a leR120 odM100 ityx 80 e lpm60 oC 40 20 0 1 '" #" )"
%" (" $" -'$.%/0*1"*2% 2 3 User ranking 4 5 6 important part. Justi cations whose intermediate inference steps arise due to the interaction between many di erent types of axioms or concept expressions are hard to understand.
Justi cations that contain unfamiliar patterns of axioms are di cult to understand. Consider the following ontology,O = f1 : A 8R:C; 2 : Domain(R; A); 3 : E v F g, which is derived from a real ontology1 and was presented to some of the study participants as part of a justi cation. This ontology entails E v A. The reason for this is that Axioms 1 and 2 entail > v A. During the study, it was observed that many of the participants (including participants with many years of experience with OWL, and even reasoner developers) did not realise, or neglected to see, that A 8R:C, coupled with Domain(R; A), entails > v A. Many of the participants had not encountered this \pattern of axioms" before. They therefore had di culty in realising what these axioms entail, and their signi cance in the context of the complete justi cation. There are, of course, other such patterns of axioms that occur in justi cations that people nd di cult to spot or understand.
A commonality between the two points detailed above is that subsets of a justi cation can result in entailments that can be viewed as \steps" or \intermediate entailments". When trying to understand justi cations, it is necessary for people to spot and understand these intermediate entailments. In terms of how complex a justi cation is for people to understand, the number of significant intermediate entailments, and for any given intermediate entailment, the number of di erent types of axioms and concept expressions that give rise to the entailment, has an e ect. What counts as a signi cant intermediate entailment is an open question; however, this basic idea of steps gives rise to the notion lemmas for justi cations. 4
Based on the data obtained from the study, we developed a simple model in order to predict how di cult it is for people to understand a given justi cation. The model is also used as a tool for identifying the signi cant intermediate inference steps in a justi cation. The model is composed of two parts: 1) A 1 This example was taken from an ontology about movies, which was originally posted to the Protege-OWL mailing list. \structural" complexity measure, which estimates the complexity based on the number of di erent types of axioms and concept expressions in a justi cation; 2) A \phenomena" based complexity measure, which increases the complexity of a justi cation when certain patterns of axioms or \phenomena" occur in the justi cation.
For the sake of brevity only an informal description and summary of the model is given here:
An \axiom and concept expression type" component estimates complexity based on the syntax of justi cations. It predicts complexity based on the number of di erent types of axioms and concept expressions in a justi cation. Di erent types of axioms, and concept expressions have di erent weightings. These weightings are based on the data obtained in the user study. For example, inverse role axioms have a heavy weighting in the complexity model because many participants found justi cations that contained inverse properties di cult to understand. Likewise, subclass axioms that have a complex concept expression on the left hand side are weighted heavier than subclass axioms that have a concept name on the left hand side.
A \signature ow" component, re ects the degree of spreading of terms in the signature of the justi cation across axioms in the justi cation (how much the signature \ ows" across the axioms in the justi cation). This component was introduced as an indicator for justi cations where there are many intermediate steps that reuse the same axioms to justify their conclusions. In some sense, it re ects the \tangling" of the justi cation.
A \universal implication" component increases the computed complexity if there are any subclass axioms that have a left hand side of 8R:C, or equivalent concept axioms which state that 8R:C is equivalent to some other concept expression. This component was motivated by the fact that many participants failed to realise that 8R:C subsumes the class of individuals that have no R successor.
A \general concept inclusion" component increases the complexity of a justication as the number of General Concept Inclusions present in laconic versions of the justi cation increases. GCIs in laconic justi cations are usually a direct indicator of an intermediate inference step that needs to be spotted.
A \synonym of top" component increases the complexity if the justi cation has any entailed synonyms of > that are not explicitly asserted. It was found that study participants were generally surprised by this kind of entailment, with most of them having trouble spotting it.
It should be noted that various weightings are used throughout the model. The purpose of these weightings is to allow individual components of the model to be altered for tuning purposes. In a user setting, it might also be possible to tune out certain components, such as the \universal implication" component, when users start to feel comfortable spotting certain patterns of axioms. In a similar vein, the model could be augmented with additional components should other patterns be discovered in the future. In any case, the model presented here is a rst approximation, and, as will be seen, is satisfactory for the purpose of lemmatising justi cations.
A version of the model was implemented using weightings based on data from the study. Figure 2 shows a plot of the user rankings that were assigned to justi cations against complexity as predicted by the model. The model prediction has a linear relationship with the rankings provided by study participants. In fact, there is a correlation of 0.8 between the two variables, which indicates a strong correlation. In what follows the model is used as a rst approximation for predicting how di cult it is for people to understand a justi cation, which in turn, is used to de ned lemmas as the notion of intermediate inference steps. 5
Given a justi cation J for an entailment , J can be lemmatised into J 0, so that J 0 is easier to understand than J 0. With this notion in hand, lemmas for justi cations can now be de ned. First, an informal de nition is given, then a more precise de nition is given in De nition 3.
Informally, a set of lemmas for a justi cation J for is a set of axioms that is entailed by J which can be used to replace some set S J to give a new justi cation J 0 = (J n S) [ for . Moreover, J 0 is simpler to understand than J . J 0 is called a lemmatisation of J .
Various restrictions are placed on the generation of the set of lemmas that can lemmatise a justi cation J . These restrictions prevent counter-intuitive lemmatisations, an example of which will be given below. Before these restrictions are discussed, it is necessary to introduce the notion of a tidy set of axioms. De nition 2 (Tidy sets of axioms). A set of axiom S is tidy if S 6j= > v ?, S 6j= A v ? for all A 2 Sig(S), and S 6j= > v A for all A 2 Sig(S).
Intuitively, a set of axioms is tidy if it is consistent, contains no synonyms of ? (where a class name is a synonym of ? with respect to a set of axioms S if S j= A v ?), and contains no synonyms of > (where a class name is a synonym of > with respect to a set of axioms S if S j= > v A).
The restrictions mandate that a set of lemmas must only be drawn from (i) the deductive closure of tidy subsets of the set S J , (ii) from the exact set of synonyms of ? or > over S.
Without the above restrictions on axioms in , it would be possible to lemmatise a justi cation J to produce a justi cation J 0 that, in isolation, is simple to understand, but otherwise bears little or no resemblance to J . For example, consider J = fA v 9R:B; B v E u 9S:C; B v D u 8S::Cg as a justi cation for A v ?. Suppose that any axioms entailed by J , could be used as lemmas (i.e. there are no restrictions on the axioms that make up ). In this example, A is unsatis able in J , meaning that it would be possible for J 0 = fA v E; A v :Eg to be a lemmatisation of J . Here, J 0 is arguably easier to understand than J , but in bears little resemblance to J . In other words, A v E and A v :E are not intuitively lemmas for J j= A v ?. Similarly, counter-intuitive results arise if lemmas are drawn from inconsistent sets of axioms, or sets of axioms that contain synonyms for >. The de nition of lemmas below, De nition 3, therefore only allows to contain axioms that are drawn from (i) the deductive closures of tidy subsets of S J (ii) the set of direct/explicit synonyms of > or ? with respect to S.
In what follows, is the `well known' structural transformation originally
de ned in [
Algorithm 1 is a practical algorithm for computing lemmatised justi cations. The algorithm requires two sub-routines: The ComputeJusti cations sub-routine returns the justi cations for an entailment that holds in a set of axioms|any \o the shelf" implementation of a justi cation nding service may be used here. The ComputeCandidateLemmas sub-routine computes a set of axioms that are entailed by tidy subsets (De nition 2) of the set of input axioms. In the implementation described in this paper, the ComputeCandidateLemmas subroutine computes lemmas that in themselves have a low complexity and hence users nd easy to understand. In particular, the implementation computes lemmas of the form A v B, C v A, A v 9R:B, Domain(R; A), A(a), (9R:A)(a) and S v R. The implementation of the routine generates these axioms and checks that they are entailed by tidy subsets of the set of input axioms. It should be noted that Algorithm 1 is non-deterministic|the output depends on the complexity model that is used to determine whether one justi cation is simpler than another, and also on the GetCandidateLemmas subroutine. The algorithm always terminates. Algorithm 1 LemmatiseJusti cation Function-1: LemmatiseJusti cation(J; ) 1: S J [ ComputeCandidateLemmas(J; ) n f g 2: justs ComputeJusti cations(S; ) 3: c1 ComputeComplexity(J; ) 4: L J 5: for J 0 2 justs do 6: c2 ComputeComplexity(J 0; ) 7: if c2 < c1 then 8: L J 0 9: return L 6.1
In order to demonstrate that it is practical to compute lemmatised justi cations, the 1 algorithm was implemented in Java using the latest version of the OWL API in conjunction with the Pellet reasoner. Justi cations (over 450 for entailments of the form A v B, A v ? and A(a)) whose predicted complexity was greater than 100.0 (roughly corresponding to `Di cult', `Very di cult' or `Impossible'), were then selected for lemmatisation from the ontologies, shown in Table 3. For each justi cation a lemmatised version of the justi cation that had a predicted complexity of less than 50.0 (roughly corresponding to a `very easy' or `easy' ranking) was computed. The implementation was run on a laptop with a 2.16GHz Intel Core Duo Processor, with the Java Virtual Machine allocated 1GB RAM. Figure 5 shows a justi cation J for Person v ?. A lemmatisation of this justi cation, along with lemmatisations of the justi cations for the lemmas over J is shown in Figure 6. Axioms in J are shown in bold, while lemmas are shown in a plain typeface. In this example, J was initially lemmatised to give J 0 = f> v Movie, Person v :Movieg. Since > v Movie is lemma in J 0, another justi cation for this lemma was computed over J and then itself lemmatised. This process was repeated to automatically build up the tree shown in Figure 6. It should be noted that this presentation is for illustrative purposes and to give a avour of the kinds of lemmas introduced into a justi cation, it is not necessarily intended for end users. 8
In [
A wide range of people can nd justi cations for entailments in OWL di cult to understand. The work that has been presented in this paper attempts to begin to address this problem through the use of lemmas for justi cations.
A model that predicts how di cult it is for people to understand a justi cation has been de ned. The model was calibrated and validated against data from a user study. This model has been used as input into a de nition of lemmas for justi cations. The de nition speci es that a lemmatisation of a justi cation results in another justi cation that is easier to understand according to the notion of justi cation complexity. Initial empirical results indicate that it is feasible to compute lemmatised justi cations for entailments from published ontologies.
The next major challenge is to design and evaluate services that make use of lemmatised justi cations for building proof structures that are ultimately aimed at end users. More studies will be needed to evaluate these mechanisms and to show that they can be bene cially integrated into ontology development environments and user work ows.