Protégé推理器中自限制公理未触发本体不一致的问题咨询

问题场景 #

在Protégé中构建了一个测试本体，包含以下元素：

• 对象属性：REL、REL1、REL2
• 个体：x
• 核心公理：
  1. x与自身存在REL1关系（x REL1 x）
  2. x与自身存在REL2关系（x REL2 x）
  3. 属性链REL1 ∘ REL2是REL的子属性（REL1 o REL2 subPropertyOf: REL）
  4. 所有满足“与自身存在REL关系”的个体类是owl:Nothing的子类（REL some Self SubClassOf owl:Nothing）

预期推导与实际结果 #

按照逻辑推导：

1. 从x REL1 x和x REL2 x，通过属性链规则可推出x REL x
2. x因此属于REL some Self类
3. 由于REL some Self是owl:Nothing的子类，x应属于空类，与x被断言为owl:Thing实例的事实矛盾，本体应处于不一致状态

但使用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)

问题原因分析 #

HermiT 1.4.3.456是较旧的版本，可能存在对属性链推导结果与ObjectHasSelf约束组合推理的支持缺陷。尝试升级到HermiT 1.5.x及以上版本，大概率能正确检测到本体的不一致性。

另外，也可以将SubClassOf(ObjectHasSelf(:REL) owl:Nothing)替换为等价的公理DisjointClasses(ObjectHasSelf(:REL) owl:Thing)，部分旧版本推理器对这种不相交约束的处理更直接。

内容的提问来源于stack exchange，提问作者Nellina