如果 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 的实例，因为他教了两门以上的课程。但是，John 只教授 2 门课程，推理者不会将他归类为 ProfessorLazy。

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

还有其他方法可以完成这项工作吗？如果某物不是ProfessorBusy，它是ProfessorLazy？

Answer 1

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

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

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

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

2. 要使 (1) 起作用，您需要说明课程数量有限：EquivalentClasses(:Course ObjectOneOf(:INF1000 :INF2000 :INF3000 :INF4000 :INF5000))