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 efficient reasoning support, facilitates ontology specification, but need not be accessible to the broad range of users. Using diagrammatic notations for reasoning, in addition to specification, can bring benefits. Standard ontology editors often support a visualization; Protégé 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 offer many of the benefits that good diagrammatic notations 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 vehicles. 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: 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: So, when a is instantiated as a particular element, e, the unlabelled curve represents 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:

(e): 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:

(g): Therefore, Mick is a person, as required:

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. 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 semantics when manipulating the syntax in an inference step. This is, perhaps, a primary advantage of reasoning with a well-designed diagrammatic logic.

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.