I am studying the inference in OWL, currently the downcast of an individual type from its property domain. I've constructed the following example ontology:
@prefix : <http://www.test.org/2015/4/ontology#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@base <http://www.test.org/2015/4/ontology> .
<http://www.test.org/2015/4/ontology> rdf:type owl:Ontology .
:Class1 rdf:type owl:Class .
:Sub1 rdf:type owl:Class ;
rdfs:subClassOf :Class1 .
:Prop1 rdf:type owl:DatatypeProperty ;
rdfs:domain :Sub1 .
:Ind1 rdf:type :Class1 , owl:NamedIndividual ;
:Prop1 "p" .
As expected the reasoner (Pellet in my case) inferred the statement that the :Ind1 is of type :Sub1:
:Ind1 :Prop1 "p"
:Prop1 rdfs:domain :Sub1
=> :Ind1 a :Sub1
Then I added the following definitions:
:Class2 rdf:type owl:Class .
:Sub2 rdf:type owl:Class ;
rdfs:subClassOf :Class2 .
:Prop2 rdf:type owl:DatatypeProperty ;
rdfs:domain [ rdf:type owl:Class ;
owl:unionOf ( :Sub1
:Sub2
)
] .
:Ind2 rdf:type :Class2 , owl:NamedIndividual ;
:Prop2 "p" .
The domain of the property :Prop2 is now either the :Sub1 or the :Sub2.
I expected also in this case that the class :Sub2 is inferred by reasoner as the type of the :Ind2. But it does not occur.
Why can't it be inferred? Where am I wrong?
I expected also in this case that the class :Sub2 is inferred by reasoner as the type of the :Ind2. But it does not occur.
Why do you expect this? The class A or B is the class of elements which are either A's or B's (or both). If you say that the domain of a property is A or B, then from a property assertion, you can infer that the subject is member of the union class A or B, but that alone isn't enough to infer that the subject is a member of A or of B.
This may be especially clear when the union class is made up of disjoint classes. For instance, imagine a property hasWings with the domain Plane or Bird. If I assert that x hasWings 2, then you know that x is either a Plane or a Bird, and thus that it is a Plane or Bird, but you don't know yet whether x is a Plane or a Bird.
You are right, belonging to domains Plane or Bird is alone not enough to infer that the X is a Plane or a Bird if it has only one feature - the property hasWings. But in my example the individual has also a second feature - the type, that is the super class of one of the classes building the union. Imagine that the Plane is subClassOf Machine and the Bird is subClassOf Animal. If we define that the X is a Machine and hasWings 2 then the type of X should be inferred to be Plane.
Just because an individual belongs to some class doesn't mean that it must belong to any particular subclasses of that class. Right now, you know that
(a) Ind2 ∈ Class2
(b) Ind2 ∈ (Sub1 ⊔ Sub2)
(c) Sub2 ⊑ Class2;
You're claiming that we should be able to infer that
Ind2 ∈ Sub2
but that's not the case. Suppose the actual interpretation of the classes is this:
Class2 ≡ {Ind2}
Sub1 ≡ {Ind2}
Sub2 ≡ {}
That's perfectly consistent with the axioms and the inferences; it makes them all true: