Explaining by Example: Model Exploration for Ontology Comprehension Johannes Bauer, Ulrike Sattler, and Bijan Parsia School of Computer Science, The University of Manchester, UK Abstract. In this paper, we describe an approach for ontology compre- hension support called model exploration in which models for ontologies are generated and presented interactively. We also discuss the issues in- volved 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 effectiveness in supporting users in understanding an ontology. 1 Motivation At different 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 fixed. Tool support is necessary to achieve these kinds of understanding, as ontologies can be as broad and complicated as the fields 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 testified 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, justifications, 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 first, 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. Nobleman Commoner i3 i2 hasSon hasSon Nobleman i1 Fig. 1: A Clarifying Example This paper is based on [1], in which we developed the notion of model ex- ploration from these observations. Informally, model exploration is the activity of interactively generating and visualizing models for concepts in ontologies in order to learn something about the concept/ontology. The details are fleshed out in Section 3. In Section 6 we report on a user study we conducted on our model exploration prototype, SuperModel, to evaluate the merits of model exploration. 2 Notation In this paper, we use standard DL terminology, syntax and semantics as defined e.g. in [2]. Additionally, we will use C and D for concept descriptions, i, i1 , i2 . . . for individual names, r for role names, R for roles, and C, R, and NI for sets of concepts, roles, and individual names. 3 Model Exploration 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 infinitely many) very big (infinitely big) models of a given concept. What we hope is that seeing small parts of just a few models suffices 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 specifi- cation, model generation, and model inspection (see Fig. 2). In the first 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 con- straint 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 first constraint ABox is obtained from the user-specified root concept Cr by adding the assertion Cr (ir ) to an empty ABox. The model excerpt always includes the root individual ir . Inspect Model Cr (ir ) Constrain Model Generate Model Fig. 2: Model Exploration Cycle 3.1 Status of Information 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 = {C(i) | C ∈ C, i ∈ NI , iI ∈ CI } ∪ {R(i, i0 ) | r ∈ R, i, i0 ∈ NI , (iI , i0I ) ∈ RI } Let I = (∆I , ·I ) be an interpretation. We then define the graph corresponding to I as the graph GI = (V, E, LV , LE ) where V = ∆I , LV : V → C 2 , LV (i) = {C ∈ C | i ∈ CI } E = V 2, LE : E → R2 , LE (e) = {R ∈ R | e ∈ RI }. It is obvious that an interpretation I and its corresponding graph GI are inter- translatable. 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 define 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 ( ( I 1 if C(i) ∈ A, I 0I 1 if R(i, i0 ) ∈ A, asrt(C, i ) = and asrt(R, (i , i )) = 0 otherwise. 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 = {(∃r.C)(ir )}. 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 define 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, (ir I , i1 I )) = 1 and mnd(C, i1 ) = 1. Now, while asserted node and edge labels are asserted independently of each other, they can only be defined to be mandatory in relation to each other: con- sider the concept definition D v ∃p.A u ∃p.B u ∃p.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 D D D ir ir ir p p p p p p A,B C A B,C A,C B i1 i2 i1 i2 i1 i2 Fig. 3: Illustration of Mandatory Information Either of the sets {D(ir ), p(ir , i1 ), A(i1 )} and {D(ir ), p(ir , i1 ), B(i1 )} could be said to be a set of mandatory axioms1 in the sense that a similar set of axioms is satisfied 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 definition 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 definition 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 define a function mnd() on node and edge labels C ∈ C and R ∈ R, resp., and nodes {iI , i0I } ⊆ ∆I , {i, i0 } ⊆ NI in a graph corresponding to I as follows: 1 modulo renaming of individuals not occurring in ontology or constraint ABox, see [1] ( ( I 1 if C(i) ∈ S, I 0I 1 if R(i, i0 ) ∈ S, mnd(C, i ) = and mnd(R, (i , i )) = 0 otherwise 0 otherwise. Let GI be the graph corresponding to an interpretation based on a com- pletion graph. If that completion graph was generated by a tableau reasoner using dependency sets for backjumping [3, 4], then a function mnd() can be de- rived from information about the dependency sets of labels in the completion graph [1]: for a label of a node or edge in GI , mnd() is 1 exactly if the dependency set for the corresponding label in the completion graph is empty. 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 Model Generation 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++ [5], a state-of-the-art, open-source tableau reasoner for the SROIQ(D) description logic, to generate models for model exploration. 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 rela- tionship 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 be- cause we wanted to test the general approach first 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 finite model property usually use blocking [10, 11] to ensure termination. A model exploration system can point out blocked nodes and blockers in the model visualization or clone blockers’ successors on demand to allow infinite exploration of a model. 2 downloadable at http://www.man.ac.uk/∼bauerj/supermodel/ Caching: caching is a common optimization technique in tableau reasoners [5]; in order for it to produce unpruned completion graphs, caching needs to be disabled in a reasoner for model exploration. Preprocessing: told cycle and synonym elimination [5] are forms of prepro- cessing which make a knowledge base easier to reason with. A consequence of these techniques is that, from a set of equivalent named concepts, only some may be in a completion graph node’s label. The others need to be added for model exploration. 5 Related Work—Tool Support for Ontology Authors A number of tools have been developed over the years to help users of ontolo- gies understand them in the broader sense. This section discusses classes and examples of these tools to get a perspective of the landscape around model ex- ploration. We group these classes into two categories: first, 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 [12],3 Protégé 4,4 and OBOEdit,5 visualizations for various purposes like the ones discussed in [13], as well as justifications [14], query tools, ontology metrics analyzers etc. are examples. Secondly, there are model inspection tools, which generate models for ontolo- gies and one way or another present them to users. An effort to generate and visualize models for OWL ontologies is described in [15], introducing the music score notation. This notation is in fact original, but it has the drawback of not being very easy on the screen size it uses for visualization, as the authors note. Tweezers [16], extracts models from the Pellet DL reasoner [17] to aid a very specific way of understanding an ontology: along with its other features, model inspection is to help finding those parts of an ontology which make it costly or impossible to reason with. Garcia et al. [18] propose a translation of ontologies from description log- ics into the Alloy Specification Language and to have models generated and presented by the Alloy Analyzer. 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 in- formation 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 infinite 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/ 6 Testing Usefulness After implementing model exploration in SuperModel, we conducted a user study [19] in order to test the usefulness of model exploration for the understanding of ontologies. For that study, we followed the procedure recommended by [20, Part II]. The details of our study’s preparation and implementation can be found in [1]. 6.1 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 first 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 entail- ment.” Hyp. 2: “SuperModel can help find out, given a concept C, what role succes- sors 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 difficult 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 first and second phase were pri- marily 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 first phase, the participants were introduced to a toy ontology that was designed specifically 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 justifications and asked to try to understand them. In case they gave up on understanding some justification, they were given the opportunity to try model exploration using SuperModel on the concepts occurring in the justification. The idea was to see whether a considerable amount of justifications that at first were too difficult could be understood with the help of model exploration. 6.3 Test Results Phase 1: the first 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. 252.83 Density 172.17 268.28 ● ● ● ●● ● ●● ● ● ●●●●●● ● ● ● ●● ● ● ● ● ● ● ● 0 200 400 600 800 Times in Seconds (30 samples) Fig. 4: Est. Density and Middle Tercile, and Average of Time needed in Phase 1 We had estimated five 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 first two terciles are well below the mark of 300s. Only a minority of five participants reported they would have preferred an- swering 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 on- tology 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 partic- ipants initially gave up on a justification, 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 definitely useful to understand entailments. Three of these were not sure. None thought either SuperModel or model exploration in general was useless and no- one believed SuperModel was definitely useful but maybe model exploration was not. Eight believed model exploration was useful for other tasks related to ontol- ogy engineering, the rest was not sure. Two participants thought SuperModel was difficult 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 benefit 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 justification 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 difficult to use. This is consistent with the fact that most participants thought its usability was at least ‘normal’. We did not find any significant 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. 7 Conclusion 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 specific reasoning algorithms affect 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 justifications. The study has also identified 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 specific reasoner used, and to enable different 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 confirm 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 find while exploring a model, an explanation of why the reasoner put this information in the completion graph and, possibly, which other options there were. References 1. Bauer, J.: Model Exploration to Support Understanding of Ontologies. Diplomar- beit, Technische Universität Dresden (2009) Advisers-Baader, F. and Lutz, C. 2. Baader, F., Nutt, W.: Basic Description Logics. [21] chapter 2 3. Horrocks, I., Hustadt, U., Sattler, U., Schmidt, R.: Computational Modal Logic. In Blackburn, P., van Benthem, J., Wolter, F., eds.: Handbook of Modal Logic. Elsevier (2006) 181–245 4. Horrocks, I.: Implementation and Optimisation Techniques. [21] chapter 9 5. Tsarkov, D., Horrocks, I.: FaCT++ Description Logic Reasoner: System Descrip- tion. In: Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006). Volume 4130 of Lecture Notes in Artificial Intelligence., Springer (2006) 292–297 6. Horrocks, I., Sattler, U.: Decidability of SHIQ with Complex Role Inclusion Ax- ioms. In: Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003), Morgan Kaufmann, Los Altos (2003) 343–348 7. Horrocks, I., Sattler, U.: Decidability of SHIQ with Complex Role Inclusion Axioms. Artificial Intelligence 160(1–2) (December 2004) 79–104 8. Horrocks, I., Kutz, O., Sattler, U.: The Even More Irresistible SROIQ. In: Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2006), AAAI Press (2006) 57–67 9. Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. J. of Auto- mated Reasoning 39(3) (2007) 249–276 10. Horrocks, I., Sattler, U., Tobies, S.: Reasoning with Individuals for the Description Logic SHIQ. In McAllester, D., ed.: Proc. of the 17th Int. Conf. on Automated Deduction (CADE 2000). Volume 1831 of Lecture Notes in Computer Science., Springer (2000) 482–496 11. Motik, B., Shearer, R., Horrocks, I.: A Hypertableau Calculus for SHIQ. In: Proc. of the 2007 Description Logic Workshop (DL 2007). Volume 250 of CEUR (http://ceur-ws.org/). (2007) 12. Kalyanpur, A., Parsia, B., Sirin, E., Cuenca Grau, B., Hendler, J.: Swoop: A Web Ontology Editing Browser. Journal of Web Semantics 4 (2005) 2005 13. Katifori, A., Halatsis, C., Lepouras, G., Vassilakis, C., Giannopoulou, E.: Ontology visualization methods—a survey. ACM Comput. Surv. 39(4) (2007) 10 14. Kalyanpur, A.: Debugging and Repair of OWL Ontologies. PhD thesis, Univer- sity of Maryland at College Park, College Park, MD, USA (2006) Adviser-James Hendler. 15. Barinskis, M., Barzdins, G.: Satisfiability Model Visualization Plugin for Deep Consistency Checking of OWL Ontologies. In Golbreich, C., Kalyanpur, A., Parsia, B., eds.: OWLED. Volume 258 of CEUR Workshop Proceedings., CEUR-WS.org (2007) 16. Wang, T., Parsia, B.: Ontology Performance Profiling and Model Examination: First Steps. In Aberer, K., Choi, K.S., Noy, N., Allemang, D., Lee, K.I., Nixon, L.J.B., Golbeck, J., Mika, P., Maynard, D., Schreiber, G., Cudré-Mauroux, P., eds.: Proceedings of the 6th International Semantic Web Conference and 2nd Asian Semantic Web Conference (ISWC/ASWC2007), Busan, South Korea. Volume 4825 of LNCS., Berlin, Heidelberg, Springer Verlag (November 2007) 589–602 17. Sirin, E., Parsia, B., Cuenca-Grau, B., Kalyanpur, A., Katz, Y.: Pellet: A Practical OWL-DL Reasoner. Journal of Web Semantics 5(2) (2007) 51–53 18. Garcia, M., Kaplunova, A., Möller, R.: Model Generation in Description Logics: What Can We Learn From Software Engineering? Technical report, Institute for Software Systems (STS), Hamburg University of Technology, Germany (2007) See http://www.sts.tu-harburg.de/tech-reports/papers.html. 19. Shneiderman, B.: Designing the User Interface: Strategies for Effective Human- Computer Interaction. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (1997) 20. Dumas, J.S., Redish, J.C.: A Practical Guide to Usability Testing. Intellect Books, Exeter, UK (1999) 21. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F., eds.: The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press (2003)