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:

(p some (A or B)) 
    ≡  
(p some A) or (p some 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:

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

(p some A) and (p some B)  
    ⊑
some P (A or B) 

Union is distributive in existentials, intersection is not.

A further simple ontology demonstrates this:

Namespace: owl = <http://www.w3.org/2002/07/owl#>
Namespace:  = <http://owl.cs.manchester.ac.uk/2008/07/sssw/facts#>

Ontology: <file:/Users/seanb/Documents/Presentations/2008/SummerSchool2008/owl.cs.manchester.ac.uk/2007/07/sssw/facts.owl>

ObjectProperty: :isFriendOf
    Annotations: 
        rdfs:label "isFriendOf",
    InverseOf: 
        :hasFriend

ObjectProperty: :hasFriend
    Annotations: 
        rdfs:label "hasFriend",
    InverseOf: 
        :isFriendOf

Class: owl:Thing

Class: :Professor
    Annotations: 
        rdfs:label "Professor",
    SubClassOf: 
        :Academic

Class: :Academic
    Annotations: 
        rdfs:label "Academic",
    SubClassOf: 
        :Person
    DisjointWith: 
        :Student

Class: :Lecturer
    Annotations: 
        rdfs:comment "",
        rdfs:label "Lecturer"
    SubClassOf: 
        :Academic
    
Class: :Student
    Annotations: 
        rdfs:label "Student",
    SubClassOf: 
        :Person
    DisjointWith: 
        :Academic

Class: :Happy
    Annotations: 
        rdfs:label "Happy",
    SubClassOf: 
        :Person

Class: :Person
    Annotations: 
        rdfs:label "Person",

Individual: :charlie
    Annotations: 
        rdfs:label "charlie",
    Types: 
        :Happy,
        :Professor

Individual: :quentin
    Annotations: 
        rdfs:comment "",
        rdfs:label "quentin"
    Types: 
        owl:Thing
    Facts: 
        :hasFriend  :bob,
        :hasFriend  :charlie

Individual: :bob
    Annotations: 
        rdfs:label "bob",
    Types: 
        :Student,
        not (:Happy)

Individual: :diane
    Annotations: 
        rdfs:label "diane",
    Types: 
        :Professor,
        not (:Happy)

Individual: :roberta
    Annotations: 
        rdfs:label "roberta",
    Types: 
        owl:Thing
    Facts: 
        :hasFriend  :bob

Individual: :zaphod
    Annotations: 
        rdfs:comment "",
        rdfs:label "zaphod"
    Types: 
        :hasFriend exactly 1 owl:Thing
    Facts: 
        :hasFriend  :charlie

Individual: :patricia
    Annotations: 
        rdfs:label "patricia",
    Types: 
        owl:Thing
    Facts: 
        :hasFriend  :arthur

Individual: :william
    Annotations: 
        rdfs:label "william",
    Types: 
        :hasFriend exactly 0 owl:Thing

Individual: :richard
    Annotations: 
        rdfs:label "richard",
    Types: 
        owl:Thing
    Facts: 
        :hasFriend  :charlie

Individual: :arthur
    Annotations: 
        rdfs:comment "",
        rdfs:label "arthur"
    Types: 
        :Happy,
        :Student

Individual: :zeke
    Annotations: 
        rdfs:comment "",
        rdfs:label "zeke"
    Types: 
        :hasFriend exactly 1 owl:Thing
    Facts: 
        :hasFriend  :bob

Individual: :yolanda
    Annotations: 
        rdfs:label "yolanda",
    Types: 
        :hasFriend exactly 2 owl:Thing
    Facts: 
        :hasFriend  :bob,
        :hasFriend  :charlie

Individual: :xanthe
    Annotations: 
        rdfs:label "xanthe",
    Types: 
        :hasFriend exactly 1 owl:Thing
    Facts: 
        :hasFriend  :arthur
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,

p some (A and B) 
    ≢
(p some A) and (p some 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:

p only (A and B) 
    ≡  
(p only A) and (p only 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

(p only A) and (p only B) 
    ⊑ (P only A) or (p only B)

p only (A and B) 
    ⊑ (p only A) or (p only B) 

(p only A) or (p only B) 
    ⊑ p only (A or B) 

Intersection is distributive in universals, union is not.