Visual Reasoning about Ontologies John Howse1 , Gem Stapleton1 , and Ian Oliver2 1 University of Brighton, UK {john.howse,g.e.stapleton}@brighton.ac.uk 2 Nokia, Helsinki, Finland ian.oliver@nokia.com Abstract. We explore a diagrammatic logic suitable for specifying on- tologies using a case study. Diagrammatic reasoning is used to establish consequences of the ontology. Introduction. The primary (formal) notations for ontology modelling are sym- bolic, such as description logics or OWL [2]. The provision of symbolic notations, along with highly efficient reasoning support, facilitates ontology specification, but need not be accessible to the broad range of users. Using diagrammatic no- tations for reasoning, in addition to specification, can bring benefits. Standard ontology editors often support a visualization; Protégé includes a plug-in visual- ization package, OWLVis, that shows derived hierarchical relationships between the concepts in the ontology and, thus, is very limited. Currently, some diagram- matic notations have been used for specifying ontologies, but they are either not formalized [3] or do not offer many of the benefits that good diagrammatic no- tations afford [4]. In [6], we proposed ontology diagrams, which we now rename concept diagrams, for ontology modelling. We extend [6] by demonstrating how one can reason using concept diagrams. Ontology Specification. We use a variation of the University of Manchester’s People Ontology [1] as a case study. It relates people, their pets and their vehi- cles. We now formally define the ontology. The diagrams below assert: (a) a man is an adult male person, (b) every van is a vehicle, and (c) every driver is an adult: adult male vehicle adult man van driver (a): (b): (c): person In (a), the shading asserts that the set man is equal to the intersection of the sets adult, male and person. Also, (d) every animal is a pet of some set of people: animal person Diagram (d) asserts that the relation isPetOf isPetOf relates animals to people, and only people: (d): a each animal a is related by the relation is- PetOf to a (possibly empty) subset of people. So, when a is instantiated as a particular element, e, the unlabelled curve rep- resents the image of isPetOf with its domain restricted to {e}. As animal and person are not disjoint concepts – a person is an animal – the curves representing these concepts are placed in separate sub-diagrams, so that no inference can be made about the relationship between them. We define the concepts of being a driver and a white van man: (e) p is a person who drives some vehicle if and only if p is a driver, and (f) m is a man who drives a white van if and only if m is a white van man: person drives vehicle man drives vehicle p p (e): (f): whiteThing driver whiteVanMan p p The two parallel, horizontal lines mean if and only if ; a single line means implies. We now introduce an individual called Mick: (g) Mick is male and drives ABC1, (h) ABC1 is a white van, and (i) Rex an animal and is a pet of Mick: male whiteThing van animal drives isPetOf (g): Mick ABC1 (h): ABC1 (i): Rex Mick Diagrammatic Reasoning. We have enough information to prove diagram- matically some lemmas, culminating in proving that Mick is a white van man. person Lemma 1 Mick is a person: Mick Proof From diagram (i) and diagram (d) we animal person isPetOf deduce all of the individuals of which Rex is a Rex Mick pet are people: person Therefore, Mick is a person, as required: Mick In the above proof, the deduction that the set of individuals of which Rex is a pet relied on pattern matching diagrams (i) and (d). We believe it is clear from the visualizations that one can make the given deduction. The last step in the proof simply deletes syntax from the diagram in the preceding step, thus weakening information, to give the desired conclusion. Much of the reasoning we shall demonstrate requires pattern matching and syntax deletion. adult Lemma 2 Mick is an adult: Mick vehicle whiteThing van Proof From diagram (b) we know that all vans ABC1 are vehicles so we deduce, from diagram (h): vehicle Therefore, ABC1 is a vehicle: ABC1 male vehicle drives From diagram (g), we therefore deduce: Mick ABC1 male vehicle Now, ABC1 is a particular vehicle. Therefore, drives Mick Mick drives some vehicle: Person vehicle drives By lemma 1, Mick is a person, thus: Mick driver Hence, by diagram (e), Mick is a driver: Mick adult driver By diagram (c) drivers are adults: Mick adult Hence, Mick is an adult, as required: Mick Lemma 3 follows from lemmas 1 and 2, together with diagrams (a) and (g) (the interested reader may like to attempt the proof): man Lemma 3 Mick is a man: Mick whiteVanMan Theorem 1 Mick is a white van man: Mick man Proof By lemma 3, Mick is a man so drives Mick ABC1 we deduce, using diagram (g): man van drives Mick From diagram (h) we have: ABC1 whiteThing man van drives Therefore Mick drives some white thing Mick which is a van: whiteThing whiteVanMan By diagram (f), we conclude that Mick Mick is a white van man: The visual reasoning we have demonstrated in the proofs of the lemmas and the theorem is of an intuitive style and each deduction step can be proved sound. We argue that intuitiveness follows from the syntactic properties of the diagrams reflecting the semantics. For instance, because containment at the syntactic level reflects containment at the semantic level, one can use intuition about the se- mantics when manipulating the syntax in an inference step. This is, perhaps, a primary advantage of reasoning with a well-designed diagrammatic logic. Conclusion. We have demonstrated how to reason with concept diagrams. The ability to support visual reasoning should increase the accessibility of inference steps, leading to better or more appropriate ontology specifications: exploring the consequences of an ontology can reveal unintended properties or behaviour. These revelations permit the ontology to be improved so that it better models the domain of interest. Our next step is to formalize the inference rules that we have demonstrated and prove their soundness. Ideally, these rules will be intuitive to human users, meaning that people can better understand why entailments hold. This complements current work on computing justifications [5] which aims to produce minimal sets of axioms from which an entailment holds; finding minimal sets allows users to focus on the information that is relevant to the deduction in question which is important when dealing with ontologies containing very many axioms. Using a visual syntax with which to communicate why the entailment holds (i.e. providing a diagrammatic proof) may allow significant insight beyond knowing the axioms from which a statement can be deduced. Acknowledgement. Supported by EPSRC grants EP/H012311, EP/H048480. Thanks to Manchester’s Information Management Group for helpful discussions. References 1. http://owl.cs.manchester.ac.uk/2009/iswc-exptut, 2009. 2. F. Baader, D. Calvanese, D. McGuinness, D. Nadi, and P. Patel-Schneider (eds). The Description Logic Handbook. CUP, 2003. 3. S. Brockmams, R. Volz, A. Eberhart, and P. Löffler. Visual modeling of OWL DL ontologies using UML. Int. Semantic Web Conference, 198–213. Springer, 2004. 4. F. Dau and P. Ekland. A diagrammatic reasoning system for the description logic ALC. Journal of Visual Languages and Computing, 19(5):539–573, 2008. 5. M. Horridge, B. Parsia, and U. Sattler. Computing explanations for entailments in description logic based ontologies. In 16th Automated Reasoning Workshop, 2009. 6. I. Oliver, J. Howse, E. Nuutila, and S. Törmä. Visualizing and specifying ontologies using diagrammatic logics. In Australasian Ontologies Workshop, 2009.