Protégé 推理机中的自我限制

Question

作为使用自我限制的练习，我在 Protégé 中实现了一个简单的本体。本体包含以下内容：

• 对象属性：REL、REL1 和 REL2；
• 个人：x；
• 公理：

  • x REL1 x

  • x REL2 x

  • REL1 或 REL2 子属性：REL

  • REL 一些猫头鹰的自子类：Nothing

我预计本体是不一致的（事实上，“x REL1 x”和“x REL2 x”意味着“x REL x”，而“x REL x”又意味着x是“REL some Self”类的成员）；但是，当我运行推理机（HermiT 1.4.3.456）时，没有显示错误。看来推理者忽略了公理“REL some Self SubClassOf owl:Nothing”。

我的本体（OWL函数语法）的主要部分报告如下：

Declaration(ObjectProperty(:REL))
Declaration(ObjectProperty(:REL1))
Declaration(ObjectProperty(:REL2))
Declaration(NamedIndividual(:x))

############################
#   Named Individuals
############################

# Individual: :x (:x)

ClassAssertion(owl:Thing :x)
ObjectPropertyAssertion(:REL1 :x :x)
ObjectPropertyAssertion(:REL2 :x :x)


SubClassOf(ObjectHasSelf(:REL) owl:Nothing)
SubObjectPropertyOf(ObjectPropertyChain(:REL1 :REL2) :REL)

Answer 1

TL;DR：使用 OWL DL 无法解释这一点。

较长的解释。

这有两个原因：

1. 推理仅适用于已知类别。 IE。类

   REL Self

   是一个匿名类，通常不会报告匿名类的推论。这是因为有无数的解释。

2. 要解决问题 1，您可以引入一个类来表示

   REL Self

   。

   Declaration(Class(:RelSelf))
   EquivalentClasses(:RelSelf ObjectHasSelf(:REL))
   

当您对此运行推理机时，您将收到一条错误，指出您在推理机的自我限制中使用了非简单角色。为了确保可判定性，支撑 OWL 2 的 DL SROIQ 限制了角色的使用。 本文详细解释了这些限制。