OWL Reasoning Examples

This version:
http://owl.man.ac.uk/2003/why/20031203
Latest version:
http://owl.man.ac.uk/2003/why/latest
Author:
Sean Bechhofer, University of Manchester

Abstract

This document presents simple example OWL ontologies and discusses some of the inferences that can be made about the classes and individuals in those ontologies.

Status of this document

This is a draft produced 3rd December, 2003. Note that the document uses mathematical symbols — these may not display correctly in Internet Explorer.

Table of contents

1. Introduction

The OWL Web Ontology Language describes a language for ontologies. This language is equipped with a formal semantics described in the OWL Web Ontology Semantics and Abstract Syntax [OWL S&AS]. Using these semantics, inferences about ontologies and individuals can be made. It is not always obvious why these inferences have occurred, however. Explanation of reasoning process is a topic of research interest — however this is still to reach a state where it is effective.

This document presents a simple example ontology and a number of illustrative examples of reasoning. Although not intended to be comprehensive, the hope is that the examples will aid users of OWL to understand why the inferences are being drawn in their ontologies.

2. Ontology

An ontology about people is available in RDF/XML. It is also shown below in abstract syntax format.

Namespace(a	= <http://cohse.semanticweb.org/ontologies/people#>)

Ontology(

 ObjectProperty(a:drives)
 ObjectProperty(a:eaten_by)
 ObjectProperty(a:eats
  inverseOf(a:eaten_by)
  domain(a:animal))
 ObjectProperty(a:has_child)
 ObjectProperty(a:has_father
  range(a:man))
 ObjectProperty(a:has_mother
  range(a:woman))
 ObjectProperty(a:has_parent)
 ObjectProperty(a:has_part
  inverseOf(a:part_of))
 ObjectProperty(a:has_pet
  domain(a:person)
  range(a:animal))
 ObjectProperty(a:is_pet_of
  inverseOf(a:has_pet))
 ObjectProperty(a:likes)
 ObjectProperty(a:part_of)
 ObjectProperty(a:reads
  range(a:publication))
 ObjectProperty(a:works_for)

 Class(a:adult partial 
  annotation(rdfs:comment "Things that are adult.")  
 Class(a:animal partial     
  restriction(a:eats someValuesFrom (owl:Thing)))
 Class(a:animal_lover complete 
  intersectionOf(restriction(a:has_pet minCardinality(3)) a:person))
 Class(a:animal_lover partial 
  annotation(rdfs:comment "Someone who really likes animals"))
 Class(a:bicycle partial 
  a:vehicle)
 Class(a:bicycle partial 
  annotation(rdfs:comment "A human propelled vehicle, with two
  wheels"))  
 Class(a:bone partial)
 Class(a:brain partial)
 Class(a:broadsheet partial 
  annotation(rdfs:comment "A newspaper. Broadsheets are usually 
  considered to be more \"high-brow\" than tabloids."))  
  a:newspaper)
 Class(a:bus partial 
  a:vehicle)
 Class(a:bus_company partial 
  a:company)
 Class(a:bus_driver complete 
  annotation(rdfs:comment "Someone who drives a bus.")
  intersectionOf(restriction(a:drives someValuesFrom (a:bus))
  a:person))
 Class(a:car partial 
  a:vehicle)
 Class(a:cat partial 
  a:animal)
 Class(a:cat_liker complete 
  intersectionOf(a:person restriction(a:likes someValuesFrom (a:cat))))
 Class(a:cat_owner complete 
  intersectionOf(a:person restriction(a:has_pet someValuesFrom (a:cat))))
 Class(a:company partial)
 Class(a:cow partial 
  annotation(rdfs:comment "Cows are naturally vegetarians.")
  a:vegetarian)
 Class(a:dog partial 
  restriction(a:eats someValuesFrom (a:bone)))
 Class(a:dog_liker complete 
  intersectionOf(restriction(a:likes someValuesFrom (a:dog)) a:person))
 Class(a:dog_owner complete 
  intersectionOf(a:person restriction(a:has_pet someValuesFrom (a:dog))))
 Class(a:driver complete 
  intersectionOf(restriction(a:drives someValuesFrom (a:vehicle)) a:person))
 Class(a:driver partial 
  a:adult)
 Class(a:duck partial a:animal)
 Class(a:elderly partial a:adult)
 Class(a:female partial)
 Class(a:giraffe partial 
  a:animal
  restriction(a:eats allValuesFrom (a:leaf)))
 Class(a:grass partial 
  a:plant)
 Class(a:grownup complete 
  intersectionOf(a:person a:adult))
 Class(a:haulage_company partial 
  a:company)
 Class(a:haulage_truck_driver complete 
  intersectionOf(restriction(a:drives someValuesFrom (a:truck)) a:person 
    restriction(a:works_for someValuesFrom 
      (restriction(a:part_of someValuesFrom (a:haulage_company))))))
 Class(a:haulage_worker complete 
  restriction(a:works_for someValuesFrom 
   (unionOf(restriction(a:part_of someValuesFrom (a:haulage_company)) 
            a:haulage_company))))
 Class(a:kid complete 
  intersectionOf(a:person a:young))
 Class(a:leaf partial 
  restriction(a:part_of someValuesFrom (a:tree)))
 Class(a:lorry partial 
  a:vehicle)
 Class(a:lorry_driver complete 
  intersectionOf(restriction(a:drives someValuesFrom (a:lorry)) a:person))
 Class(a:mad_cow complete 
  annotation(rdfs:comment "A mad cow is a cow that has been eating the
  brains of sheep.") 
  intersectionOf(restriction(a:eats someValuesFrom 
    (intersectionOf(restriction(a:part_of someValuesFrom (a:sheep)) a:brain))) a:cow))
 Class(a:magazine partial 
  a:publication)
 Class(a:male partial 
   annotation(rdfs:comment "The class of all male things."))
 Class(a:man complete 
  intersectionOf(a:male a:person a:adult))
 Class(a:newspaper partial 
  annotation(rdfs:comment "All newspapers are either broadsheets or tabloids.")
  a:publication
  unionOf(a:tabloid a:broadsheet))
 Class(a:old_lady complete 
  intersectionOf(a:female a:person a:elderly))
 Class(a:old_lady partial 
  intersectionOf(restriction(a:has_pet allValuesFrom (a:cat)) 
                 restriction(a:has_pet someValuesFrom (a:animal))))
 Class(a:person partial 
  a:animal)
 Class(a:pet complete 
  restriction(a:is_pet_of someValuesFrom (owl:Thing)))
 Class(a:pet_owner complete 
  intersectionOf(restriction(a:has_pet someValuesFrom (a:animal)) a:person))
 Class(a:plant partial)
 Class(a:publication partial)
 Class(a:quality_broadsheet partial a:broadsheet)
 Class(a:red_top partial a:tabloid)
 Class(a:sheep partial 
  a:animal
  restriction(a:eats allValuesFrom (a:grass)))
 Class(a:tabloid partial 
  annotation(rdfs:comment "A newspaper. Tabloids are usually thought of
as more "down-market" than broadsheets.")
  a:newspaper)
 Class(a:tiger partial 
  a:animal)
 Class(a:tree partial 
  a:plant)
 Class(a:truck partial 
  a:vehicle)
 Class(a:van partial 
  a:vehicle)
 Class(a:van_driver complete 
  intersectionOf(restriction(a:drives someValuesFrom (a:van)) a:person))
 Class(a:vegetarian complete 
  annotation(rdfs:comment "A vegetarian is defined as an animal that
  eats no other animals, or parts of animals.")
  intersectionOf(a:animal 
    restriction(a:eats allValuesFrom (complementOf(restriction(a:part_of someValuesFrom (a:animal))))) 
    restriction(a:eats allValuesFrom (complementOf(a:animal)))))
 Class(a:vehicle partial)
 Class(a:white_thing partial)
 Class(a:white_van_man complete 
  annotation(rdfs:comment "A white van man is a man who drives a white van.")
  intersectionOf(restriction(a:drives someValuesFrom (intersectionOf(a:van a:white_thing))) a:man))
 Class(a:white_van_man partial 
  restriction(a:reads allValuesFrom (a:tabloid)))
 Class(a:woman complete 
  intersectionOf(a:female a:person a:adult))
 Class(a:young partial)
 Class(owl:Thing partial)

 AnnotationProperty(rdfs:comment)
 AnnotationProperty(rdfs:label)

 Individual(a:Daily_Mirror annotation(rdfs:comment "The paper read by Mick (a white van man).")
  type(owl:Thing))
 Individual(a:Dewey type(a:duck))
 Individual(a:Fido type(a:dog))
 Individual(a:Flossie type(a:cow))
 Individual(a:Fluffy type(a:tiger))
 Individual(a:Fred type(a:person)
  value(a:has_pet a:Tibbs))
 Individual(a:Huey type(a:duck))
 Individual(a:Joe type(a:person)
  type(restriction(a:has_pet maxCardinality(1)))
  value(a:has_pet a:Fido))
 Individual(a:Kevin type(a:person)
  value(a:has_pet a:Fluffy)
  value(a:has_pet a:Flossie))
 Individual(a:Louie type(a:duck))
 Individual(a:Mick
  annotation(rdfs:comment "Mick is male and drives a white van. Due to
  the axiom concerning drivers, we know that Mick must be a man, and
  is therefore a white van man. The axiom about the reading material
  of a white van man then allows us to infer things about the Daily
  Mirror.")
  type(a:male)
  value(a:reads a:Daily_Mirror)
  value(a:drives a:Q123_ABC))
 Individual(a:Minnie type(a:female) type(a:elderly)
  value(a:has_pet a:Tom))
 Individual(a:Pete type(owl:Thing))
 Individual(a:Q123_ABC
  annotation(rdfs:comment "A white van")
  type(a:van)
  type(a:white_thing))
 Individual(a:Rex type(a:dog)
  value(a:is_pet_of a:Mick))
 Individual(a:Spike type(owl:Thing)
  value(a:is_pet_of a:Pete))
 Individual(a:The_Guardian type(a:broadsheet))
 Individual(a:The_Sun type(a:tabloid))
 Individual(a:The_Times type(a:broadsheet))
 Individual(a:Tibbs type(a:cat))
 Individual(a:Tom type(owl:Thing))
 Individual(a:Walt type(a:person)
  value(a:has_pet a:Huey)
  value(a:has_pet a:Louie)
  value(a:has_pet a:Dewey))

 AllDifferent(a:Daily_Mirror a:Dewey a:Fido a:Flossie a:Fluffy a:Fred
  a:Huey a:Joe a:Kevin a:Louie a:Mick a:Minnie a:Pete a:Q123_ABC 
  a:Rex a:Spike a:The_Guardian a:The_Sun a:The_Times a:Tibbs
  a:Tom a:Walt)

 DisjointClasses(unionOf(a:animal restriction(a:part_of someValuesFrom (a:animal))) 
  unionOf(a:plant restriction(a:part_of someValuesFrom (a:plant))))
 DisjointClasses(a:tabloid a:broadsheet)
 DisjointClasses(a:adult a:young)
 DisjointClasses(a:cat a:dog)

 SubPropertyOf(a:has_mother a:has_parent)
 SubPropertyOf(a:has_father a:has_parent)
 SubPropertyOf(a:has_pet a:likes)
)

3. Class Inferences

Bus Drivers are Drivers

Class(a:bus_driver complete intersectionOf(a:person
  restriction(a:drives someValuesFrom (a:bus))))

Class(a:driver complete intersectionOf(a:person
  restriction(a:drives someValuesFrom (a:vehicle))))

Class(a:bus partial a:vehicle)

The subclass is inferred due to subclasses being used in existential quantification.

Cat Owners like Cats

Class(a:cat_owner complete intersectionOf(a:person
  restriction(a:has_pet someValuesFrom (a:cat))))

SubPropertyOf(a:has_pet a:likes)

Class(a:cat_liker complete intersectionOf(a:person
  restriction(a:likes someValuesFrom (a:cat))))

The subclass is inferred due to a subproperty assertion.

Drivers are Grown Ups

(Note: A grown up is an adult person)

Class(a:driver complete intersectionOf(a:person
  restriction(a:drives someValuesFrom (a:vehicle))))

Class(a:driver partial a:adult)

Class(a:grownup complete intersectionOf(a:adult a:person))

An example of axioms being used to assert additional necessary information about a class. We do not need to know that a driver is an adult in order to recognize one, but once we have recognized a driver, we know that they must be adult.

Sheep are Vegetarians

Class(a:sheep partial 
  restriction(a:eats allValuesFrom (a:grass))
  a:animal)

Class(a:grass partial a:plant)

DisjointClasses(unionOf(restriction(a:part_of someValuesFrom (a:animal)) a:animal) 
                          unionOf(a:plant restriction(a:part_of someValuesFrom (a:plant))))

Class(a:vegetarian complete intersectionOf(
    restriction(a:eats allValuesFrom (complementOf(restriction(a:part_of someValuesFrom (a:animal))))) 
    restriction(a:eats allValuesFrom (complementOf(a:animal))) a:animal))

Note the complete definition, which means that we can recognise when things are vegetarians.

Giraffes are Vegetarians

 Class(a:giraffe partial a:animal
  restriction(a:eats allValuesFrom (a:leaf)))

 Class(a:leaf partial restriction(a:part_of someValuesFrom (a:tree)))
 Class(a:tree partial a:plant)

DisjointClasses(unionOf(restriction(a:part_of someValuesFrom (a:animal)) a:animal) 
                          unionOf(a:plant restriction(a:part_of someValuesFrom (a:plant))))

Class(a:vegetarian complete intersectionOf(
    restriction(a:eats allValuesFrom (complementOf(restriction(a:part_of someValuesFrom (a:animal))))) 
    restriction(a:eats allValuesFrom (complementOf(a:animal))) a:animal))

Similar to the previous example with the additional inference provided by the existential restriction in the definition of leaf

Old Ladies own Cats

Class(a:old_lady complete 
  intersectionOf(a:person a:female a:elderly))

Class(a:old_lady partial intersectionOf(
  restriction(a:has_pet allValuesFrom (a:cat)) 
  restriction(a:has_pet someValuesFrom (a:animal))))

Class(a:cat_owner complete intersectionOf(a:person
  restriction(a:has_pet someValuesFrom (a:cat))))

An example of the interaction between an existential quantification (asserting the existence of a pet) and a universal quantification (constraining the types of pet allowed).

This also illustrates that an ontology is one view on the world — you may disagree with my modelling but I am being explicit about it.

Mad Cows are inconsistent

Class(a:cow partial a:vegetarian)

DisjointClasses(unionOf(restriction(a:part_of someValuesFrom (a:animal)) a:animal) 
                          unionOf(a:plant restriction(a:part_of someValuesFrom (a:plant))))

Class(a:vegetarian complete intersectionOf(
    restriction(a:eats allValuesFrom (complementOf(restriction(a:part_of someValuesFrom (a:animal))))) 
    restriction(a:eats allValuesFrom (complementOf(a:animal))) a:animal))

Class(a:mad_cow complete intersectionOf(a:cow 
  restriction(a:eats someValuesFrom (intersectionOf(restriction(a:part_of someValuesFrom (a:sheep)) 
                                                                                   a:brain)))))

Class(a:sheep partial a:animal
  restriction(a:eats allValuesFrom (a:grass)))

Thus a mad cow has been eating part of an animal, which is inconsistent with the definition of a vegetarian

4. Instance Inferences

The Daily Mirror is a Tabloid

 Individual(a:Daily_Mirror type(owl:Thing))

 Individual(a:Mick type(a:male)
  value(a:drives a:Q123_ABC)
  value(a:reads a:Daily_Mirror))

 Individual(a:Q123_ABC type(a:van) type(a:white_thing))

 Class(a:white_van_man complete 
  intersectionOf(a:man restriction(a:drives someValuesFrom (intersectionOf(a:van a:white_thing)))))
 Class(a:white_van_man partial restriction(a:reads allValuesFrom (a:tabloid)))

Here we see interaction between complete and partial definitions plus a universal quantification allowing an inference about a role filler.

Pete is a Person, Spike is an Animal

Individual(a:Spike type(owl:Thing)
  value(a:is_pet_of a:Pete))

Individual(a:Pete
  type(owl:Thing))

ObjectProperty(a:has_pet domain(a:person) range(a:animal))

ObjectProperty(a:is_pet_of inverseOf(a:has_pet))

Here we see an interaction between an inverse relationship and domain and range constraints on a property.

Walt loves animals

Individual(a:Walt type(a:person)
  value(a:has_pet a:Huey)
  value(a:has_pet a:Louie)
  value(a:has_pet a:Dewey))

Individual(a:Huey type(a:duck))
Individual(a:Dewey type(a:duck))
Individual(a:Louie type(a:duck))

DifferentIndividuals(a:Huey a:Dewey a:Louie)

Class(a:animal_lover complete intersectionOf(a:person restriction(a:has_pet minCardinality(3))))

Note that in this case, we don’t actually need to include person in the definition of animal lover (as the domain restriction will allow us to draw this inference).

Tom is a Cat

Individual(a:Minnie type(a:female) type(a:elderly) value(a:has_pet a:Tom))

Individual(a:Tom type(owl:Thing))

ObjectProperty(a:has_pet domain(a:person) range(a:animal))

Class(a:old_lady complete 
  intersectionOf(a:person a:female a:elderly))

Class(a:old_lady partial intersectionOf(
  restriction(a:has_pet allValuesFrom (a:cat)) 
  restriction(a:has_pet someValuesFrom (a:animal))))

Here the domain restriction gives us additional information which then allows us to infer a more specific type. The universal quantification then allows us to infer information about the role filler.

5. Distribution Rules

Distribution rules for existential quantification are similar to those that we encounter in propositional logic for conjunction and disjunction, e.g.

A ⊓ (B ⊔ C) ≡ (A ⊓ B) ⊔ (A ⊓ C)

Existentials

We have the following:

∃p.(A ⊔ B) ≡ (∃p.A) ⊔ (∃p.B)

In terms of OWL, this translates to:

restriction(some p unionOf(A B)) 
    ≡  
unionOf(restriction(some (p A)) 
        restriction(some (p B)))

There are also a number of inferences that are weaker than the equivalence:

∃p.(A ⊓ B) ⊑ (∃p.A) ⊓ (∃p.B)
(∃p.A) ⊓ (∃p.B) ⊑ (∃p.A) ⊔ (∃p.B)
(∃p.A) ⊓ (∃p.B) ⊑ ∃p.(A ⊔ B)

In OWL terms:

restriction(some p intersectionOf(A B) 
    ⊑
intersectionOf(restriction(some (p A)) 
               restriction(some (p B)))

intersectionOf(restriction(some (p A)) 
               restriction(some (p B))) 
    ⊑
unionOf(restriction(some (p A)) 
        restriction(some (p B)))

intersectionOf(restriction(some (p A)) restriction(some (p B))) 
    ⊑
restriction(some p unionOf(A B)

Union is distributive in existentials, intersection is not.

A second simple ontology demonstrates this:

Namespace(a	= <http://oiled.man.example.net/facts#>)

Ontology(

 ObjectProperty(a:hasFriend)
 ObjectProperty(a:isFriendOf
  inverseOf(a:hasFriend))

 Class(a:Academic partial 
  a:Person)
 Class(a:Academic partial)
 Class(a:Happy partial a:Person)
 Class(a:Happy partial)
 Class(a:Lecturer partial a:Academic)
 Class(a:Person partial)
 Class(a:Professor partial a:Academic)
 Class(a:Student partial a:Person)

 AnnotationProperty(rdfs:comment)
 AnnotationProperty(rdfs:label)

 Individual(a:Arthur type(a:Happy) type(a:Student))
 Individual(a:Bob type(complementOf(a:Happy)) type(a:Student))
 Individual(a:Charlie type(a:Professor) type(a:Happy))
 Individual(a:Diane type(a:Professor) type(complementOf(a:Happy)))
 Individual(a:Patricia
  type(owl:Thing)
  value(a:hasFriend a:Arthur))
 Individual(a:Quentin
  type(owl:Thing)
  value(a:hasFriend a:Bob)
  value(a:hasFriend a:Charlie))
 Individual(a:Richard
  type(owl:Thing)
  value(a:hasFriend a:Charlie))
 Individual(a:Roberta
  type(owl:Thing)
  value(a:hasFriend a:Bob))
 Individual(a:William
  type(restriction(a:hasFriend cardinality(0))))
 Individual(a:Xanthe
  type(restriction(a:hasFriend cardinality(1)))
  value(a:hasFriend a:Arthur))
 Individual(a:Yolanda
  type(restriction(a:hasFriend cardinality(2)))
  value(a:hasFriend a:Bob)
  value(a:hasFriend a:Charlie))
 Individual(a:Zaphod
  type(restriction(a:hasFriend cardinality(1)))
  value(a:hasFriend a:Charlie))
 Individual(a:Zeke
  type(restriction(a:hasFriend cardinality(1)))
  value(a:hasFriend a:Bob))

 AllDifferent(a:Arthur a:Bob a:Charlie a:Diane a:Patricia
   a:Quentin a:Richard a:Roberta a:William a:Xanthe a:Yolanda
   a:Zaphod a:Zeke) 

 DisjointClasses(a:Academic a:Student)
)

The ontology contains some basic classes, Person, Academic, Professor and Student. There is also a subclass of Happy Persons and an axiom stating that Students and Academics are disjoint. Note that we can infer that Professors and Students are disjoint due to the disjointness axiom concerning Academics and Students. The four individuals Arthur, Bob, Diane and Charlie then occupy different partitions of the domain.

The other individuals now provide witnesses for the non-equivalence of the definitions. For example,

restriction(some p intersectionOf(A B)) 
    ≢
intersectionOf(restriction(some (p A)) restriction(some (p B)))

Quentin has a friend who is Happy (Charlie) and a friend who is a Student (Bob). However, Quentin is not known to have a friend who is both Happy and a Student. We are able to infer that Quentin is an instance of the second class, but not of the first. Thus their extensions are not the same.

Universals

Rules for universal quantification are similar.

∀p.(A ⊓ B) ≡ (∀p.A) ⊓ (∀p.B)

In terms of OWL, this translates to:

restriction(all p intersectionOf(A B)) 
    ≡  
intersectionOf(restriction(all (p A)) 
        restriction(all (p B)))

There are again a number of inferences that are weaker than the equivalence:

(∀p.A) ⊓ (∀p.B) ⊑ (∀p.A) ⊔ (∀p.B)
∀p.(A ⊓ B) ⊑ (∀p.A) ⊔ (∀p.B)
(∀p.A) ⊔ (∀p.B) ⊑ (∀p.(A ⊔ B))

in OWL

intersectionOf(restriction(all (p A)) 
               restriction(all (p B))) 
    ⊑
unionOf(restriction(all (p A)) 
        restriction(all (p B))) 

restriction(all p intersectionOf(A B) 
    ⊑
unionOf(restriction(all (p A)) 
        restriction(all (p B))) 

unionOf(restriction(all (p A)) 
        restriction(all (p B))) 
    ⊑
restriction(all p unionOf(A B)

Intersection is distributive in universals, union is not.

6. Closed and Open Worlds

Individual(a:Patricia value(a:hasFriend a:Arthur))

In the example, we find that Patricia is not an instance of

restriction(all friends intersectionOf(Student Happy))

This is due to the open world assumption (OWA). We cannot assume that if we don’t know something then it is false. In this example, there may be other friends that Patricia has that are not Students. Reasoning in DLs is monotonic — if we know that x is an instance of A, then adding more information to the model cannot cause this to become false.

Some of the individuals in the ontology have additional cardinality constraints which close the relation, allowing us to make further inferences about all the friends they have.

Individual(a:Xanthe type(restriction(a:hasFriend cardinality(1))) 
  value(a:hasFriend a:Arthur))

Thus Xanthe is an instance of:

restriction(all friends intersectionOf(Student Happy))

as we know all the friends that she has (and they all match the description).

Empty Quantification

A common source of confusion in OWL semantics is when we have universal quantification over an empty set.

Individual(a:William type(restriction(a:hasFriend cardinality(0))))

In this case, we know that William has no friends. So William is an instance of:

restriction(all friends intersectionOf(Student Happy))

and

restriction(all friends unionOf(Student Happy))

In fact he’s an instance of 

restriction(all friends X)

for any class description X (even Nothing).

Universal quantification over an empty collection is trivially true.

.

References

[OWL S&AS]
OWL Web Ontology Language Semantics and Abstract Syntax. Peter F. Patel-Schneider, Patrick Hayes, Ian Horrocks. W3C Candidate Recommendation 18 August 2003.