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 further simple ontology demonstrates this:

Namespace(a	= <http://owl.man.ac.uk/2005/sssw/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 intersectionOf(restriction(some (hasFriend Happy)) restriction(some (hasFriend Student))), but not of restriction(some hasFriend intersectionOf(Student Happy)). 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.