如果a与B互斥，并且个体不在B中，那么OWL本体中的个体如何被归类为a的实例

Question

这是我用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)
)

不出所料，推理者正确地将Marc归类为ProfessorBusy的实例，因为他教授了2门以上的课程。然而，John只教授2门课程，推理者不会将其归类为ProfessorLazy。

我猜，由于开放世界的假设，我们永远不能确定约翰实际教授的课程是否少于2门。

有其他方法可以做到这一点吗？如果某个东西不是ProfessorBusy，它就是ProfessorLazy？

Answer 1

推理器不推断John是ProfessorLazy的原因是由于开放世界假设。开放世界假设基本上意味着推理者只能根据明确陈述的信息或可以从明确陈述信息中得出的信息进行推理。推理者无法对其他任何事情做出任何判断。

这就是为什么推理者不能推断John是ProfessorLazy。可以肯定的是，约翰教授两门课程。没有资料表明John只教授2门课程。推理者认为约翰教授的课程有可能是目前未知的。

为了得到你想要的，你需要关闭这个世界。这正是@Stanislav Kralin的评论所说的。

1. 您需要声明John没有教授任何其他课程：NegativeObjectPropertyAssertion(:teaches :John :INF3000)等。

2. 为了(1(工作，你需要说明课程数量有限：EquivalentClasses(:Course ObjectOneOf(:INF1000 :INF2000 :INF3000 :INF4000 :INF5000))