Search code examples
owlprotegeinference

How can an individual in a OWL ontology be classified as an instance of A, if A is mutually exclusive to B and the individual is not in B?

Here is my ontology created with Protege.

Prefix(:=<http://www.semanticweb.org/kolam/ontologies/2020/9/exInference#>)
Prefix(owl:=<http://www.w3.org/2002/07/owl#>)
Prefix(rdf:=<http://www.w3.org/1999/02/22-rdf-syntax-ns#>)
Prefix(xml:=<http://www.w3.org/XML/1998/namespace>)
Prefix(xsd:=<http://www.w3.org/2001/XMLSchema#>)
Prefix(rdfs:=<http://www.w3.org/2000/01/rdf-schema#>)


Ontology(<http://www.semanticweb.org/kolam/ontologies/2020/9/exInference>

Declaration(Class(:Course))
Declaration(Class(:Professor))
Declaration(Class(:ProfessorBusy))
Declaration(Class(:ProfessorLazy))
Declaration(ObjectProperty(:hasChild))
Declaration(ObjectProperty(:teaches))
Declaration(NamedIndividual(:INF1000))
Declaration(NamedIndividual(:INF2000))
Declaration(NamedIndividual(:INF3000))
Declaration(NamedIndividual(:INF4000))
Declaration(NamedIndividual(:INF5000))
Declaration(NamedIndividual(:John))
Declaration(NamedIndividual(:Marc))

############################
#   Classes
############################

# Class: :Professor (:Professor)

EquivalentClasses(:Professor ObjectSomeValuesFrom(:teaches :Course))

# Class: :ProfessorBusy (:ProfessorBusy)

EquivalentClasses(:ProfessorBusy ObjectIntersectionOf(:Professor ObjectComplementOf(:ProfessorLazy)))

# Class: :ProfessorLazy (:ProfessorLazy)

EquivalentClasses(:ProfessorLazy ObjectIntersectionOf(:Professor ObjectMaxCardinality(2 :teaches :Course)))


############################
#   Named Individuals
############################

# Individual: :INF1000 (:INF1000)

ClassAssertion(:Course :INF1000)

# Individual: :INF2000 (:INF2000)

ClassAssertion(:Course :INF2000)

# Individual: :INF3000 (:INF3000)

ClassAssertion(:Course :INF3000)

# Individual: :INF4000 (:INF4000)

ClassAssertion(:Course :INF4000)

# Individual: :INF5000 (:INF5000)

ClassAssertion(:Course :INF5000)

# Individual: :John (:John)

ObjectPropertyAssertion(:teaches :John :INF1000)
ObjectPropertyAssertion(:teaches :John :INF2000)

# Individual: :Marc (:Marc)

ObjectPropertyAssertion(:teaches :Marc :INF3000)
ObjectPropertyAssertion(:teaches :Marc :INF4000)
ObjectPropertyAssertion(:teaches :Marc :INF5000)


DifferentIndividuals(:INF1000 :INF2000 :INF3000 :INF4000 :INF5000)
)

As expected, the reasoner correctly classifies Marc as an instance of ProfessorBusy since he teaches more than 2 courses. However, John teaches only 2 courses and the reasoner won't classify him as a ProfessorLazy.

I'm guessing that because of the open world assumption, we are never sure that John actually teaches less than 2 courses.

Is there another way to make this work ? If something is not a ProfessorBusy, it is a ProfessorLazy ?

Solution

  • The reason why the reasoner does not infer that John is a ProfessorLazy is due to the open world assumption. The open world assumption basically means that the reasoner can only make inferences based on explicitly stated information or information that can be derived from explicitly stated information. Anything else the reasoner cannot make any judgement on.

    That is why the reasoner cannot infer that John is ProfessorLazy. All it knows for sure is that John teaches 2 Courses. There is no information that states that John teaches ONLY 2 courses. The reasoner assumes there is a possibility that John is teaching a course that is just unknown currently.

    For getting what you want, you need to close the world. That is in essence what @Stanislav Kralin's comment is saying.

    1. You need to state that John does not teach any of the other course: NegativeObjectPropertyAssertion(:teaches :John :INF3000) etc.

    2. For (1) to work you need to state that there are a limited number of courses: EquivalentClasses(:Course ObjectOneOf(:INF1000 :INF2000 :INF3000 :INF4000 :INF5000))