Description Logic representation that requires the modelling of sameness or distiction of two individuals

I am trying to model the following statement in Description Logic.

A co-teaching faculty member is any person who is an academic staff and teaches at least one course that is taught by others

The representation that I have thought of is: CoTeachingFaculty EQUIV Person INTERSECTION AcademicStaff EXISTS teaches.(Course INTERSECTION EXISTS isTaughtBy.TOP)

I have a feeling that this is an incorrect representation as EXISTS isTaughtBy.TOP will connect an individual with itself via the chain x--teaches-->c--isTaughtBy-->x. Thus even if a faculty does not share a course with others, she will belong to the class CoTeachingFaculty.

Thus it is required to establish a chain x--teaches-->c--isTaughtBy-->y where x and y are different. Will it be possible to model this kind of situation in the Description Logic framework?

Solution

Yes, you are quite correct that your representation will not have the desired effect.

There are possibly 2 ways that I can think of that will achieve more-or-less what you want:

(1) Introduce a coTeachesWith role which is irreflexive and define teaches as teaches \sqsubseteq coTeachesWith o teaches. In this way you can state that a lecturer co-teaches with another lecturer and from that you can infer that teach the same courses. The downside is that it will infer that all classes taught by this lecturer are also taught by the co-teaching lecturer - which is likely not what you want.

(2) Another way is to use SWRL rules. With that you can provide a rule as follows:

teaches(?x, ?c) ^ teaches(?y, ?c) ^ differentFrom(?x, ?y) ->

CoTeachingFaculty(?x) ^ CoTeachingFaculty(?y)

Below I provide the OWL Manchester syntax for the ontology applying these 2 options:

Prefix: : http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual# 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# Prefix: xml: http://www.w3.org/XML/1998/namespace Prefix: xsd: http://www.w3.org/2001/XMLSchema#

Ontology: <http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual>
<http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual/0.0.1>

AnnotationProperty: <http://swrl.stanford.edu/ontologies/3.3/swrla.owl#isRuleEnabled>   
AnnotationProperty: rdfs:comment
AnnotationProperty: rdfs:label
Datatype: xsd:boolean
Datatype: xsd:string

ObjectProperty: coTeachesWith
    Characteristics: Irreflexive
    Domain: CoTeachingFaculty
    Range: CoTeachingFaculty

ObjectProperty: isTaughtBy
    Domain: Course
    Range: AcademicStaff
    
ObjectProperty: teaches
    SubPropertyChain: coTeachesWith o teaches
    Domain: AcademicStaff
    Range: Course
    
Class: AcademicStaff
    SubClassOf: Person,
        teaches some Course
    
Class: CoTaughtCourse
    EquivalentTo: isTaughtBy min 2 owl:Thing
    SubClassOf: Course
    
Class: CoTeachingFaculty
    SubClassOf: AcademicStaff
    
Class: Course
    DisjointWith: Person
    
Class: Person
    DisjointWith: Course
    
Class: owl:Thing    

Individual: course1
    Types: Course
    Facts:  
     isTaughtBy  lecturer1,
     isTaughtBy  lecturer2
    DifferentFrom: course2
    
Individual: course2
    Types: Course
    DifferentFrom: course1
    
Individual: course3

Individual: lecturer1
    Facts:  coTeachesWith  lecturer2
    DifferentFrom: lecturer2
    
Individual: lecturer2
    Facts:  
     teaches  course1,
     teaches  course2
    DifferentFrom: lecturer1
    
Individual: lecturer3
    Facts:  teaches  course2
    DifferentFrom: lecturer4
    
Individual: lecturer4
    Facts:  teaches  course2
    DifferentFrom: lecturer3
    
DifferentIndividuals: 
    course1,course2,course3

Rule: 
    teaches(?<http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual#x>, ?<http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual#c>), teaches(?<http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual#y>, ?<http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual#c>),  DifferentFrom (?<http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual#x>, ?<http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual#y>) -> CoTeachingFaculty(?<http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual#x>), CoTeachingFaculty(?<http://www.henrietteharmse.com/turtorial/ontologies/DistinctIndividual#y>)

PS. I did not set teaches to be the inverse of taughtBy because then teaches is no longer a simple role and then cannot be used in a role chain. For details see paper on SROIQ.