In this paper, we describe an approach for ontology comprehension support called model exploration in which models for ontologies are generated and presented interactively. We also discuss the issues involved in using tableau reasoners for the generation of models for model exploration and report on a user study we conducted on our prototype implementation, SuperModel, to evaluate its e ectiveness in supporting users in understanding an ontology.
At di erent stages of an ontology's life-cycle, the people working with it require some sort of understanding of it; e.g. which parts of it encode what piece of knowledge explicitly or implicitly, how it is meant to be used on its own or in conjunction with other ontologies, and if and where it is broken and how it may be xed. Tool support is necessary to achieve these kinds of understanding, as ontologies can be as broad and complicated as the elds of knowledge they model, and as it is easy to get lost in the highly complex interactions between the large numbers of logical axioms they comprise.
This need is testi ed and partially met by the impressive tool support which has recently become available. However, support facilitates use and use spawns demand for more support. Thus, the very increase in popularity of ontology engineering brought about by ontology editors, visualization, justi cations, etc. may be seen as one reason for the demand for even more support.
Looking at anecdotal evidence, we found that some DL experts liked to use pen and paper to visualize models of ontologies to explain or check some of their lesser obvious implications. Our idea was that the automatic generation and presentation of such models could similarly aid the understanding of ontologies.
Think, for example, of an ontology stating that a Nobleman is someone who is the son of a Nobleman, and a Commoner is someone who is not a Nobleman. One might be surprised to see that a Commoner can have a son who is a Nobleman. However, the example depicted in Fig. 1, where that Nobleman is at the same time the son of both a Commoner and a Nobleman, should immediately clear up the situation and make it obvious that the ontology lacks a statement saying that no-one can be son of two men.
Problems like the one discussed above may creep up even if one has a fair understanding of the ontology in question because rst, in order to understand, in our example, why a Nobleman may have a Commoner father, one would have to know what axioms to look at, and secondly keep track of the possibly complex interactions of these axioms|or theyr failure to interact.
i2 hasSon
hasSon
i3 i1
This paper is based on [
In this paper, we use standard DL terminology, syntax and semantics as de ned
e.g. in [
The idea behind model exploration is that it may be useful for users to see models of concepts in an ontology to understand their semantics. Unfortunately, there may be very many (even in nitely many) very big (in nitely big) models of a given concept. What we hope is that seeing small parts of just a few models su ces in many cases to give users the information they seek. This is why model exploration includes an interactive component which lets the user decide which parts of what models to see.
Model exploration is an activity cycling through the stages of model speci cation, model generation, and model inspection (see Fig. 2). In the rst stage, the users add axioms to an ABox which serve as constraints for the type of model they want to see next. In model generation, a completion graph for this constraint ABox is computed and adorned with additional information. In model inspection, a connected subgraph, the model excerpt, of this completion graph is presented graphically to the user and may be expanded (explored) along the edges of the completion graph.
The rst constraint ABox is obtained from the user-speci ed root concept Cr by adding the assertion Cr(ir) to an empty ABox. The model excerpt always includes the root individual ir.
Cr(ir)
To make the presentation of the rest of this section easier, we will assume, without loss of generality, models in which, for every individual in its domain, there is an individual name which it maps to that individual. We can then refer to individuals in an interpretation by their individual name and describe interpretations and their corresponding graphs by sets of ABox axioms in a straightforward manner: we say that A describes an interpretation I, if A = fC(i) j C 2 C; i 2 NI ; iI 2 CI g
[ fR(i; i0) j r 2 R; i; i0 2 NI ; (iI ; i0I ) 2 RI g
Let I = ( I ; I ) be an interpretation. We then de ne the graph corresponding to I as the graph GI = (V; E; LV ; LE ) where
V =
I ; E = V 2;
LV : V ! C2; LV (i) = fC 2 C j i 2 CI g
2
LE : E ! R ; LE (e) = fR 2 R j e 2 RI g: It is obvious that an interpretation I and its corresponding graph GI are intertranslatable.
A model for an ABox must satisfy all of the ABox's axioms, and thus it is easy to see that an ABox always is a subset of every set A describing a model for it. This lets us de ne a function asrt(), for `asserted', on edge- and node labels of a graph GI corresponding to a model I for an ABox A:
Let C be a concept, R a role and i, i0 individual names. Then asrt(C; iI ) = (1 if C(i) 2 A; 0 otherwise.
and asrt(R; (iI ; i0I )) = (1 if R(i; i0) 2 A; 0 otherwise.
Another observation is that, for some ABoxes, there are assertions which are in every set describing a model for these ABoxes, but not in the ABoxes themselves. In fact, we would like to generalize this: consider the models for the ABox A = f(9r:C)(ir)g. In all models for A, ir will have an r-successor which is a C. Thus, all models of A satisfy an axiom r(ir; i1) for varying individual names i1.
This is a commonality which we believe is worth pointing out when visualizing a model. Thus, we would like to de ne a function mnd(), for `mandatory', on node and edge labels such that, if, in a model, i1 is the name of that r-successor, then mnd(r; (irI ; i1I )) = 1 and mnd(C; i1) = 1.
Now, while asserted node and edge labels are asserted independently of each other, they can only be de ned to be mandatory in relation to each other: consider the concept de nition D v 9p:A u 9p:B u 9p:C u 2 p and the models depicted in Fig. 3, which are the alternatives created for D by a standard tableau reasoner.
(a) Alternative 1 (b) Alternative 2 (c) Alternative 3 A,B p i1
D ir p
C i2
A p i1
D ir p
B,C i2
A,C p i1
D ir p
B i2
Either of the sets fD(ir); p(ir; i1); A(i1)g and fD(ir); p(ir; i1); B(i1)g could be said to be a set of mandatory axioms1 in the sense that a similar set of axioms is satis ed by every model of D.
No such set should contain the axioms A(i1) and B(i1), because in other models, the p-successors of the instance of D which are an A and a B, respectively, are not the same, as can be seen in Figs. 3b and 3c.
In order to be useful for users of model exploration, a de nition for labels being mandatory needs to be simple enough to work with in practice, yet capture a meaningful notion of commonalities of all models of an ontology and a concept. We believe that the following de nition strikes a good compromise:
A set of ABox axioms S is a mandatory superset of an ABox A w.r.t. an ontology O, if S includes A and every model for A and O can be transformed into a model for O and all the axioms in S only by changing its interpretation of individual names occurring in S but not in A or O.
For a model I of an ABox A and a mandatory superset S of A, we de ne
a function mnd() on node and edge labels C 2 C and R 2 R, resp., and nodes
fiI ; i0I g I ; fi; i0g NI in a graph corresponding to I as follows:
1 modulo renaming of individuals not occurring in ontology or constraint ABox, see [
Let GI be the graph corresponding to an interpretation based on a
completion graph. If that completion graph was generated by a tableau reasoner
using dependency sets for backjumping [
Our prototype implementation of model exploration, SuperModel,2 follows the approach described in this section and uses dependency sets to obtain a mandatory superset and include it in its visualization of models. 4
For a model to be explored, it must be generated. Since model generation is
the basis of tableau reasoning in DLs, there is a large body of work dealing
with exactly this problem|we used FaCT++ [
We said model generation was the basis of tableau reasoning, because the completion graphs generated by today's reasoners have a certain correspondence with models but they are not equivalent. Also, certain optimizations employed in automatic reasoners make the information found in these graphs incomplete from the point of view of model exploration. This section deals with the issues involved in using practical tableau reasoners to generate completion graphs for model exploration.
Complex Roles: the trouble with transitive roles and general role inclusion axioms (RIA) for model exploration is that tableau algorithms usually treat transitivity and RIAs rather indirectly [6{9].
Thus, completion graphs do not always contain an edge for every role relationship in the corresponding model. In order to be able to visualize models, these role relationships need to be added. This is easy for simple super-roles. We left adding roles implied by transitivity or general RIAs for future work because we wanted to test the general approach rst before going into the details of how to accommodate the possibly large numbers of additional arcs in our visualization.
Blocking: tableau algorithms for DLs which lack the nite model property
usually use blocking [
Preprocessing: told cycle and synonym elimination [
A number of tools have been developed over the years to help users of ontologies understand them in the broader sense. This section discusses classes and examples of these tools to get a perspective of the landscape around model exploration.
We group these classes into two categories: rst, and predominantly, there
are axiom inspection tools, whose purpose it is to make the axioms of an ontology
and their logical implications more accessible. Ontology editors like Swoop [
Secondly, there are model inspection tools, which generate models for ontologies and one way or another present them to users.
An e ort to generate and visualize models for OWL ontologies is described
in [
Tweezers [
Garcia et al. [
None of these model inspection tools allow users to add constraints on the models as described in Section 3 or show anything similar to the status of information we discuss in Section 3.1. The relevant papers also do not report on any empiric evidence of usefulness in general ontology engineering tasks. Only Tweezers supports in nite models by marking blocked nodes (although without pointing out the blockers). 3 http://code.google.com/p/swoop/ 4 http://www.co-ode.org/downloads/protege-x/ 5 http://oboedit.org/
After implementing model exploration in SuperModel, we conducted a user study
[
Hypotheses A study tests hypotheses. A user study tests hypotheses about the usability and usefulness for a particular set of applications of a piece of software. The hypotheses must be formulated such that they are testable and relevant to the software's intended use.
We rst collected a number of hypotheses about what SuperModel could be useful for, and then, due to the limited time for the user study, selected the following three hypotheses that we most expected to get positive results for: Hyp. 1: \SuperModel can be used to understand the reason for a given entailment." Hyp. 2: \SuperModel can help nd out, given a concept C, what role successors an instance of C must/may/may not have and which concepts they must/may/may not be instances of, and the same about their successors." Hyp. 3: \When using SuperModel, a user can gain knowledge circumstantial to the task at hand."
Since we also wanted to see whether model exploration was a good method to gain knowledge in these ways, and because we wanted to know, in case of negative results, whether the problem lied with model exploration or with the implementation, we tested the following hypotheses, which we hoped to refute: Hyp. 4: \It is di cult to use model exploration to acquire information about an ontology." Hyp. 5: \The complexity of the user interface of SuperModel is high compared to the actual tasks which it is designed to facilitate." 6.2
Experiments We conducted our user study in two phases. The rst and second phase were primarily meant to test Hyps. 2, and 1, respectively. We gathered evidence relating to Hyp. 3 and specializations of Hyps. 4 and 5 along the way. The instruments used to gather data were experimenter's observations, logging of clicks and times, and questionnaires throughout the experiments.
In the rst phase, the participants were introduced to a toy ontology that was designed speci cally for this user study. They were then shown how SuperModel might be used to answer a question in the style of Hyp. 2, before being asked to try and answer three similar questions about that ontology.
In the second phase, they were presented justi cations and asked to try to understand them. In case they gave up on understanding some justi cation, they were given the opportunity to try model exploration using SuperModel on the concepts occurring in the justi cation. The idea was to see whether a considerable amount of justi cations that at rst were too di cult could be understood with the help of model exploration. 6.3
Test Results Phase 1: the rst phase of the study went fairly successfully: out of the twelve participants, only two could not answer all of the questions presented to them satisfactorily. Only two reported they did not enjoy using SuperModel for the tasks presented to them in this phase of the study.
y it s n e D
We had estimated ve minutes acceptable to answer the kinds of questions we asked with a unfamiliar tool. Fig. 4 shows a distribution density function estimated from our thirty samples, the gray area indicates the middle tercile of the function and the mark at 252.83s shows the average of our test results. The rst two terciles are well below the mark of 300s.
Only a minority of ve participants reported they would have preferred answering the questions some other way. Comparison with demographic data from the questionnaires shows that the group of those who preferred SuperModel over other methods had a higher percentage of self-reported experts in the use of ontology editors and a lower percentage of self-reported experts of formal logics. Also, the two failures to answer one of the questions asked in this phase fall into the group of logic experts who were not ontology editor experts. Phase 2: out of 58 samples collected in Phase 2, 32 were cases in which participants initially gave up on a justi cation, out of which 15 were then eventually understood after activating SuperModel.
In the questionnaire following the understanding of a task after activating SuperModel, SuperModel was fully credited with giving the relevant clues only once. However, in ten cases, participants reported it gave them "some of the clues" necessary to understand the entailment.
No conclusive evidence was collected supporting Hyp. 3.
Post-Test Questionnaire: seven participants thought model exploration was de nitely useful to understand entailments. Three of these were not sure. None thought either SuperModel or model exploration in general was useless and noone believed SuperModel was de nitely useful but maybe model exploration was not.
Eight believed model exploration was useful for other tasks related to ontology engineering, the rest was not sure. Two participants thought SuperModel was di cult to use; three found it easy, the rest thought it normal. 6.4
Interpretation The data for Phase 1 of the experiment suggests that the kind of question asked in it can indeed be answered in acceptable time using SuperModel. Together with the demographic data it also suggests that the bene t from SuperModel increases with familiarity with ontology editors and decreases with knowledge about formal logics.
The reason for the former could be that users of ontology editors are used to graphical environments that actively support them in the understanding of ontologies. The latter may be caused by experts of formal logics having developed their own strategies for extracting information from logical theories.
The fact that, in Phase 2, almost half of the cases where participants could not understand a justi cation on its own were understood with SuperModel is encouraging. However, in more than half of those cases, they spent considerably more time with SuperModel than we hoped they would, and only in two thirds of the cases they credited SuperModel with giving them at least some of the clues they needed.
The measures on usability of SuperModel's UI suggest that there is room for improvement, but also that the problems are not so grave as to make it di cult to use. This is consistent with the fact that most participants thought its usability was at least `normal'.
We did not nd any signi cant evidence supporting Hyp. 3. The reason for this may have been that the ontologies were very simple and contained little information that could have been learned in addition to what was necessary.
In this paper, we have introduced model generation, a technique for supporting ontology engineers in their understanding of ontologies. We have explained how structures similar to models can be extracted from tableau reasoners and how the speci c reasoning algorithms a ect the models and additional information found in these structures. We have discussed the issues and choices involved in implementing model exploration and produced a prototype whose usefulness was assessed in a user study.
The results of this study are encouraging: they suggest that model exploration can indeed help users answer certain questions about an ontology and, to a certain degree, to understand justi cations.
The study has also identi ed starting points for future work both on our implementation and on model exploration in general.
On the Prototype: we would like to further develop SuperModel to improve usability, make it more independent of the speci c reasoner used, and to enable di erent styles of use.
On Testing Usefulness: although it did yield valuable results, the study we report on in this paper is only a pilot study in scope. More pilot studies and experience with model exploration is needed to identify probable strengths of model exploration and ways to con rm them in an in-depth user study with more intense experiments. Apart from that, the use of mandatory information should be evaluated.
On Model Exploration: we would like to explore the possibilities and options for handling transitive roles and general role inclusion axioms. Also, it would be very interesting to investigate means to give users, for a piece of information they nd while exploring a model, an explanation of why the reasoner put this information in the completion graph and, possibly, which other options there were.