This paper describes the explanation in OWL landscape. In recent years there has been huge progress, both in theory and implementation, in the area of explaining the causes of entailments in OWL ontologies. This paper charts the course of explanation in OWL and then looks at ways in which user understanding of ontologies might be further improved. Speci cally, the use of ne-grained justi cations, augmentation of justi cations with lemmas, and the provision of browseable models are discussed as methods of further improving user understanding in the context of ontologies and entailments.
In 2003, as the Web Ontology Language OWL [
Both OILed and Protege had little in the way of support for debugging ontologies. It was not possible to obtain explanations as to why classes were unsatis able. The best debugging support that was available at the time was the practice of painting unsatis able classes in red, which made them relatively easy to spot. In turn, this allowed users to manually \trace" through the ontology so as to spot patterns and locate the part of the ontology that they should concentrate on when trying to understand the reasons for, and get rid of, the unsatis able classes. If a class was unsatis able, users would usually look to see if any of the super-classes were unsatis able and then concentrate on those. Likewise, they would check to see if the llers of any existential restrictions were unsatis able, and if so, navigate to these, and then attempt to spot why they were unsatis able. Having narrowed down the axioms on which they should concentrate on, many users would then start to `rip out' axioms from the ontology. Most notably people would remove disjoint classes axioms, in an attempt to rid an ontology of any unsatis able classes.
All in all, debugging an ontology that contained unsatis able classes was a
wretched and error prone process. So much so that in some cases, users were
afraid to use a reasoner to check their ontologies. At worst, for OWL, users
would switch to a di erent or legacy knowledge representation language such as
Frames [
Since the early days of OWL, there have been huge advancements in the
debugging facilities provided by ontology development environments. Most
notably, the ontology editor Swoop [
The purpose of this paper is to review work in the area of debugging and explanation for OWL ontologies, take a look at debugging support in the mainstream ontology editors, peek at current state of the art work on explanation, and nally speculate on possible future directions for explanation and debugging support. 2 2.1
OWL-DL and OWL 2
OWL-DL is a avour of OWL that corresponds to the description logic SHOIN (D).
OWL 2, which corresponds to the description logic SROIQ(D), is the latest
version of OWL that enhances OWL-DL to make it more expressive by adding new
kinds of class constructors and axioms. Herein, OWL is now used to refer to
OWL 2. It is assumed that the reader is familiar with the various OWL class
constructors and axioms. For an in-depth review of OWL the interested reader
is referred to [
The semantics of OWL is given by interpretations. Interpretations explicate the relationship between syntax and semantics. An interpretation, I = h I ; I i, is tuple that consists of a non-empty interpretation domain, I , and an interpretation function, I . The interpretation function maps each class name A into a subset AI of the domain, each property name P into a subset RI of a binary relation over the domain, and each individual name a into to an object aI in the domain. The interpretation function is extended to deal with complex class descriptions and axioms. If an interpretation satis es every axiom in an ontology O then the interpretation is said to be a model of O.
Example Consider a very small ontology containing a single axiom O = fCar v V ehicleg. Let I = fx0g (that is, the interpretation domain I contains one object x0) and let Car and V ehicle be interpreted as follows: CarI = fx0g, V ehicle = ;. This particular interpretation is not a model of O because x0 is not in the interpretation of V ehicle and hence the interpretation does not satisfy the axiom Car v V ehicle. However, the interpretation CarI = fx0g, V ehicle = fx0g is a model of O because it satis es all axioms in O. 2.2
In what follows terminology that is related to the eld of explanation and debugging is reviewed. Ontologies that are incoherent, because they contain unsatis able classes, or ontologies that are inconsistent because they do not have any models, generally arise as the result of modelling errors. Entailments such as classes being unsatis able, or ontologies being inconsistent are usually viewed as being undesirable entailments.
Signature The signature of an ontology O is the set of class, property and individual names that are used in axioms in O. For example, consider O = fA v 9R:C; B v 8S:Dg, where the signature of O is fA; R; C; B; S; Dg. Unsatis able Classes A class is unsatis able (with respect to an ontology) if it cannot possibly have any instances in any model of that ontology. More precisely, a class is unsatis able if and only if it is interpreted as the empty set in all models. Since unsatis able classes are always interpreted as the empty set, and the empty set is a subset of every set, then an unsatis able class is a subclass of every class. In description logic notation, C v ? means that C is unsatis able.
Incoherent Ontologies In the context of debugging and explanation, an incoherent ontology is an ontology that contains at least one unsatis able class. More precisely, an ontology O is incoherent if and only if O j= C v ? for at least one class name C in the signature of O.
Inconsistent Ontologies An ontology O is inconsistent if and only if O does not have any model. An inconsistent ontology entails > v ?. It should be noted that an ontology that just contains unsatis able classes (other than >) is not inconsistent.
Entailment We write O j= if all models of O also satisfy . In this case \O entails ", and we also say that is an entailment in O. A standard description logic reasoner test each class for (un)satis ability, each ontology for consistency and can answer various entailment queries.
Justi cations Justi cations are a type of explanation for entailments in ontologies.
Let O be an ontology and any arbitrary entailment, such that O j= (O entails ). Then J is a justi cation for in O if J O, J j= and for any J 0 J J 0 6j= . Intuitively, a justi cation for an entailment in an ontology, is a minimal subset of the ontology that is su cient for the entailment in question to hold. A justi cation is minimal in the sense that for any proper subset of the justi cation, the entailment in question does not hold.
Root and Derived Unsatis able classes A class C that is unsatis able with respect to an ontology O is a derived unsatis able class if there exists a justi cation J for O j= C v ?, and a justi cation J 0 for O j= D v ? such that J J 0. A class that is not a derived unsatis able class is known as a root unsatis able class. An unsatis able class, all of whose justi cations are supersets of at least one justi cation for another unsatis able class is known as a pure derived unsatis able class.
In a nutshell, derived unsatis able classes have justi cations that are supersets of the justi cations for some other unsatis able class in the same ontology. If an unsatis able class does not have any justi cations that are supersets of justi cations for some other unsatis able class then the class is a root unsatis able class. The signi cance of this is that a user should aim to repair root unsatis able classes before repairing all other unsatis able classes because some or all derived unsatis able classes may also be repaired in the process of doing this. 3
The rst tool to bring sound and complete explanation generation facilities to end users was Swoop. The comprehensive debugging and repair facilities in this tool go a long way in addressing many of the issues identi ed in the previous section. Given an incoherent ontology, a user is able to determine the root/derived unsatis able classes so that they know which classes to concentrate on xing. They can then browse justi cations for these unsatisifable classes in order to attempt to understand why the classes are unsatis able. Finally they can use the repair tool in Swoop to suggest a repair plan for the ontology that will ultimately result in all unsatis able classes turning satis able.
An example justi cation, for DN A ?, as displayed in Swoop, is shown in Figure 1. As can be seen, Swoop presents justi cations as ordered indented lists of axioms. However, these are only based on heuristics|there hasn't been any research into an optimal ordering of axioms. For a given axiom, the right hand side (RHS) of the axiom is established and then examined so that any names appearing in the RHS signature are used to indicate which axioms should immediately follow and be indented. Broadly speaking, explanation tools in ontology development environments should ideally satisfy the following use cases. Each use case is a task that a user of a tool that generated explanations might want to accomplish. 1. Understanding entailments|A user browsing an ontology notices an entailment and opportunistically decides to obtain an explanation for the entailment in order to get a feel as to why the entailment holds. 2. Debugging and repair|A user is faced with an incoherent ontology, or an ontology that contains some other kind of undesirable entailment, and they need to determine the causes of the entailments in order to generate a repair plan. 3. Ontology comprehension|A user is faced with an ontology that they haven't seen before. In order to get a better picture of the ontology they use various metrics such as the number of entailments, the average number of justi cations for an entailment and so on. This helps them to build up an image of how complex the ontology is in terms of expressivity. Is also provides them with more information if they need to decide whether they like the ontology or not. 4. Understanding justi cations|Once a justi cation for an entailment in an ontology has been obtained, a user wants to understand the justi cation better. For example, they would like to know what entailments arise from the justi cation and which axioms within the justi cation itself cause the entailments to hold.
Over the past few years, ontology development environments have gone from no support for these tasks through to respectable support for Tasks 1 and 2. Indeed, since Swoop set the bar for explanation and repair facilities in ontology development environments, other tools have slowly begun to o er similar facilities. However, taking tools in this area into consideration, there are still some holes that need to be lled. In particular, it is arguable that the use of explanations and justi cations for ontology comprehension, and the ability to gain more insight and understanding into the justi cations themselves are still under-supported tasks. The remainder of the paper discusses work in progress in the eld of explanation and understanding of OWL ontologies. 5
Due to the typical construction of rich ontologies, and the way in which ontology development environments display and make it easy to edit axioms, it is frequently the case that axioms can be rather long. Hence, justi cations can contain \long" axioms, where only part of the axioms are required for the entailment in question to hold. In many cases, these parts can obfuscate the true reasons as to why an entailment holds. Justi cations that contain long axioms could also result in information being unnecessarily lost when repairing an ontology through deleting axioms, because it isn't clear which parts of the axioms contribute to the entailment explained by the justi cation.
The ontology editor Swoop uses heuristics to strike out class, property and individual names that are super uous to an entailment. An example of strikeout in action is shown in Figure 2, where the names process, contains and isomers have been struck out. This has the advantage of focusing the users attention on the relevant parts of the justi cation.
Justi cations that contain axioms that do not contain any redundant parts
have been known as ne-grained justi cations [
We have de ned laconic justi cations, which informally, are justi cations
that only consist of axioms that do not contain any super uous parts and whose
parts are as small and as weak as possible. Precise justi cations can be derived
from laconic justi cations, and contain axioms that are as small, at and as weak
as possible. Laconic justi cations are aimed at improving understanding, while
precise justi cations are aimed at guiding the construction of a semantically
minimal repair (see [
This work on precise justi cations resulted in some surprising results when
experiments were performed on several publicly available ontologies. For
example, for some ontologies, it was found that for a given entailment, the number
of laconic justi cations were fewer in number than the number of regular
justications. Examples were also found where regular justi cations masked further
laconic justi cations. Full details are available in [
While justi cations have proved to be incredibly useful for end users when debugging ontologies, preliminary experimental evidence suggests that, in many cases, even with justi cations in hand, users can still nd it di cult to understand the causes of entailments. The exact reasons for this are unknown. However, in the course of observing users who are tying to understand justi cations, it has been 1 Accepted as a paper in the research track at ISWC this year.
quale v 9atomic-part-of.region atomic-part-of v part-of part-of v part region v 8part.region quale v atomic-part-of.region atomic-part-of v atomic-part atomic-part v part region v 8part.region noted that there are certain justi cations that seem di cult for most users to understand. The authors hypothesise that these justi cations contain non-obvious (\hidden") entailments, and in order to understand the whole justi cation, a user must spot these non-obvious entailments.
An example of such a case is shown in Figure 4 which is taken from an ontology about movies that was posted to the Protege mailing list 2. In this example, the justi cation for P erson v M ovie also entails that the class M ovie is equivalent to T hing, and hence every class is a subclass of M ovie. However, this isn't explicit in the justi cation, and for most people this is far from obvious, yet it is critical to realise that this entailment holds in order to understand the explanation.
P arentalAdvSuggested hasV iolenceLevel domain M ovie
(1) (2) (3) (4) (5)
One possible solution is to augment justi cations with automatically generated lemmas. These lemmas can help to bridge the gap in understanding, highlighting the non-obvious entailments that are required in order to understand a justi cation. What lemmas should be used in what context is presently unknown. In order to come up with a recipe for augmenting justi cations with lemmas, an investigation is under way to determine the factors that make justi cations di cult to understand. It is hoped that this will result in a model for the complexity of understanding a justi cation. With this model in hand, it should then be possible to start to identify whether or not a justi cation is di cult to understand and decide which parts of the justi cation should be bridged with lemmas. It is expected that lemmas will be useful for an immediate 2 http://thread.gmane.org/gmane.comp.misc.ontology.protege.owl/22321/focus=22370 overview of a justi cation and allow a user to \drill down" into the justi cation should they require more understanding of the entailment or the need to carry out a repair of the ontology. As an example, some of the axioms in Figure 4 could be replaced as follows: axiom 2 could be rewritten to make it more laconic and to show a negated existential restriction so that it becomes :9hasV iolenceLevel:> v P arentalAdvisorySuggested, axiom 4 (the property domain axiom) could be rewritten to make the existential implication explicit so that it becomes 9hasV iolenceLevel> v M ovie, and axioms 4 and 5 could be replaced with one axiom P arentalAdvSuggested v M ovie. 6
Another possible strategy for users attempting to get a grasp on an ontology and the kinds of entailments that hold in it is for them to think about models. Many people nd the notion of models very natural, and are perfectly happy to browse diagrams of blobs connected by lines. Figure 5 shows a screenshot of \SuperModel", which is a new prototype tool for browsing models of class descriptions. The tool allows users to select a class description (from the hierarchy on the left hand side) and then shows a model of the class description, rooted at the \rootIndividual" instance, on the right hand side. Arcs labelled with the names of properties represent relationships to other individuals. Users of tools such as Protege tend to be not unfamiliar with such visualisations, because they have seen components that can display similar diagrams of an ontology. However, this is where the similarity with other visualisation tools ends. Because SuperModel displays models generated by description logic reasoners, it is capable of showing entailed relationships between individuals and entailed types of individuals. By clicking on a node in the graph, a user is able to view the classes that an individual, which is represented by the node, belongs to.
In the example in Figure 5 the class M argherita has been selected from the pizza ontology. SuperModel shows an example of a model for M argherita. It is easy to see that an individual that is a M argherita (pizza) has two hasT opping relationships and that one of these hasT opping successors has a hasCountryOf Origin successor to an individual that is Italy. SuperModel allows the user to gradually expand the model in order to fully explore it.
One possible use of SuperModel is that it could be used to given an indication of the reasons for non-subsumption. A frequent question on mailing lists is \Why isn't X inferred to be a subclass of Y?". In such situations, SuperModel is able to generate example models that are \counter-models" that show how an individual could be an instance of the subclass (X) and not an instance of the superclass Y . At this stage, we are investigating whether or not the use of counter-models as an aid in understanding the reasons for non-subsumption is of bene t to a typical ontology modeller. Over the past few years since OWL became a standard, services and tools for generating explanations of entailments have come from nothing to being more than respectable. In particular, the ability to generate justi cations for entailments is now seen as a key inference service that is required for the development of ontologies. However, anecdotal evidence suggests that certain types of justi cations can be very hard if not impossible for a broad range of users to understand. Work to remedy this situation includes identifying super uous parts of axioms using so-called laconic justi cations, experimenting with augmenting justi cations with lemmas, and the use of models for improving ontology understanding and comprehension.