We explore a diagrammatic logic suitable for specifying ontologies using a case study. Diagrammatic reasoning is used to establish consequences of the ontology. Introduction. The primary (formal) notations for ontology modelling are symbolic, such as description logics or OWL [2]. The provision of symbolic notations, along with highly e±cient reasoning support, facilitates ontology speci¯cation, but need not be accessible to the broad range of users. Using diagrammatic notations for reasoning, in addition to speci¯cation, can bring bene¯ts. Standard ontology editors often support a visualization; Prot¶eg¶e includes a plug-in visualization package, OWLVis, that shows derived hierarchical relationships between the concepts in the ontology and, thus, is very limited. Currently, some diagrammatic notations have been used for specifying ontologies, but they are either not formalized [3] or do not o®er many of the bene¯ts that good diagrammatic notations a®ord [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 Speci¯cation. We use a variation of the University of Manchester's People Ontology [1] as a case study. It relates people, their pets and their vehicles. We now formally de¯ne 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: a
vehicle van (c): adult driver (a): (d): adult
male man 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: person
relates animals to people, and only people: each animal a is related by the relation is
So, when a is instantiated as a particular element, e, the unlabelled curve represents the image of isPetOf with its domain restricted to f g 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 de¯ne 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: The two parallel, horizontal lines mean if and only if ; a single line means implies.
male (g): Mick Diagrammatic Reasoning. We have enough information to prove diagrammatically some lemmas, culminating in proving that Mick is a white van man.
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 adult man male male man drives ABC1
man
Mick drives
ABC1 whiteVanMan van van 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 re°ecting the semantics. For instance, because containment at the syntactic level re°ects containment at the semantic level, one can use intuition about the semantics 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 speci¯cations: 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 justi¯cations [5] which aims to produce minimal sets of axioms from which an entailment holds; ¯nding 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 signi¯cant 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. LoIJer. 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ÄormaÄ. Visualizing and specifying ontologies using diagrammatic logics. In Australasian Ontologies Workshop, 2009.