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)
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 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.
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.