如果 A 与 B 互斥并且该个体不在 B 中,那么 OWL ontology 中的个体如何归类为 A 的实例?

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?

这是我用 Protege 创建的 ontology。

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

正如预期的那样,推理器正确地将 Marc 分类为 ProfessorBusy 的实例,因为他教授超过 2 门课程。但是,John 只教授 2 门课程,推理者不会将他归类为 ProfessorLazy

我猜,由于开放世界的假设,我们永远无法确定 John 实际教授的课程少于 2 门。

还有其他方法可以实现吗?如果某物不是 ProfessorBusy,它是 ProfessorLazy ?

推理者之所以没有推断出John是一个ProfessorLazy,是因为开放世界的假设。开放世界假设基本上意味着推理者只能根据明确陈述的信息或可以从明确陈述的信息中得出的信息进行推理。推理者无法做出任何判断的其他任何事情。

这就是为什么推理者不能推断出 JohnProfessorLazy 的原因。它所知道的只是约翰教授 2 门课程。没有信息表明 John 仅教授 2 门课程。推理者假设 John 可能正在教授一门目前未知的课程。

为了得到你想要的,你需要关闭世界。这实际上就是@Stanislav Kralin 的评论所说的。

  1. 您需要声明 John 不教授任何其他课程:NegativeObjectPropertyAssertion(:teaches :John :INF3000)

  2. 对于 (1),您需要声明课程数量有限:EquivalentClasses(:Course ObjectOneOf(:INF1000 :INF2000 :INF3000 :INF4000 :INF5000))