owlontologyprotegereasonerhermit

Using only constraint in owl leads to inconsistency

I am trying to model the following situation:

I want to experiment with the usage of the "only" restriction, therefore I have defined Bachelor, for example, as equivalent to "has only BachelorStudent". Therefore, I generated the following code using Protegé:

:has rdf:type owl:ObjectProperty ;
    rdfs:domain :Degree ;
    rdfs:range :Student .

:Bachelor rdf:type owl:Class ;
    owl:equivalentClass [ rdf:type owl:Restriction ;
                          owl:onProperty :has ;
                          owl:allValuesFrom :BachelorStudent
                        ] ;
    rdfs:subClassOf :Degree ;
    owl:disjointWith :Master .

:BachelorStudent rdf:type owl:Class ;
    rdfs:subClassOf :Student ;
    owl:disjointWith :MasterStudent .

:Degree rdf:type owl:Class ;
    owl:disjointWith :Student ;
    owl:disjointUnionOf ( :Bachelor
                          :Master
                        ) .

:Master rdf:type owl:Class ;
    owl:equivalentClass [ rdf:type owl:Restriction ;
                          owl:onProperty :has ;
                          owl:allValuesFrom :MasterStudent
                        ] ;
    rdfs:subClassOf :Degree .

:MasterStudent rdf:type owl:Class ;
    rdfs:subClassOf :Student .

:Student rdf:type owl:Class ;
    owl:disjointUnionOf ( :BachelorStudent
                          :MasterStudent
                        ) .

However, this leads to an inconsistency when I launch the reasoner. The provided explanation is the following: Explanation for inconsistency I cannot figure out what I am doing wrong. Am I misunderstanding the use of "only", or are there any other mistakes?

Solution

  • The problem is the following: with the axiom:

    Master EquivalentTo has only MasterStudent

    it follows that things that do not have the has property are classified as Master (has only MasterStudent contains the things that do not have the has property at all). If this sounds strange, think of the class hasChild only Person. This class identifies the things such that, if they have children, then the children are people. Clearly, people belong to this class, even if they do not have children.

    The same is true for Bachelor. So, if a thing does not have the has property, it must belong to both Bachelor and Master. But if such a thing existed, then it would violate the disjointness relation between Bachelor and Master. So we must conclude that everything has the has property. This means that everything is a Degree (because of the domain of has) and is related to a Student (because of the range of has). So there exists students, and since everything is a Degree, these students are degrees, which violates the disjointness between Student and Degree.

    Now, the problem with your model is that you use an equivalence axiom. You should instead use a subclass relation, and add that all degrees must have the has relation with at least some students, like this:

    Master SubClassOf has only MasterStudent
Master SubClassOf has some Student
Bachelor SubClassOf has only BachelorStudent
Bachelor SubClassOf has some Student

    or even, if you want it more constrained:

    Master EquivalentTo (has only MasterStudent and has some Student)
Bachelor EquivalentTo (has only MasterStudent and has some Student)