owl - 如果 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 门。

还有其他方法可以使这项工作吗？如果某物不是 a ProfessorBusy，它是一个ProfessorLazy?

Answer 1

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

这就是推理者无法推断的John原因ProfessorLazy。它所知道的只是约翰教了两门课程。没有信息表明John只教授 2 门课程。推理者假设约翰可能正在教授一门目前未知的课程。

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

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

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