=Paper=
{{Paper
|id=None
|storemode=property
|title=Visual Reasoning about Ontologies
|pdfUrl=https://ceur-ws.org/Vol-658/paper455.pdf
|volume=Vol-658
|dblpUrl=https://dblp.org/rec/conf/semweb/HowseSO10
}}
==Visual Reasoning about Ontologies==
https://ceur-ws.org/Vol-658/paper455.pdf
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.