OWL 公理：给定一个特定类的个体，强制与另一个个体存在对象属性关系答案

【问题标题】：OWL axiom: Given an individual of a particular class, enforce an existence of an Object Property relation with another individualOWL 公理：给定一个特定类的个体，强制与另一个个体存在对象属性关系
【发布时间】：2018-08-17 10:45:01
【问题描述】：

在 OWL 中，有没有办法声明特定类别的个体必须通过特定对象属性与另一个个体相关联？

例如，我想说：

forall(x) Object(x) -> exists(y) Shape(y) ^ hasShape(x, y)

即“对于所有对象，都存在一个形状就是对象的形状。”

所以如果有一个对象类型的个体没有与之关联的形状，推理器会发现它是不一致的。

我尝试了一个公理：

Object SubClassOf hasShape min 1 Shape

但它不起作用。

问题似乎是因为 OWL 中的 Object Property 没有标识，但是有解决此问题的方法吗？

（我正在使用 Protege 5.2.0）

【问题讨论】：

“它不工作”是什么意思？ “OWL 中的对象属性没有身份”是什么意思？您在伪一阶逻辑公理中所写的内容与您在 OWL 公理中所写的内容完全相同。
推理器在您的案例中没有发现任何不一致之处。 OWL 推理是关于推理，而不是约束验证。还有其他方法可以处理这个问题，例如颗粒 ICV、SHACL 等 ...
@AntoineZimmermann 不工作是指推理器没有发现不一致。

标签： owl protege

【解决方案1】：

Object SubClassOf hasShape min 1 Shape 的含义是正确的，Object 的每个个体都通过hasShape 属性与Shape 的个体相关联。

那么，如果你创建了一个Object 类型的个体x，而x 没有与Shape 的个体相关联，为什么推理器不能确定你的本体不一致？原因在于开放世界假设。非正式地，这意味着推理者可以从本体中做出的唯一推论是基于本体中陈述的明确信息或可以从明确陈述的信息中得出的信息。

当您声明 x 是 Object 时，本体中没有明确信息声明 x 与Shape 通过 hasShape 属性。要明确x 不是这样的关系，您必须将x 定义如下：

Individual: x
  Types: 
    Object,
    hasShape max 0 owl:Thing

顺便说一句，这个问题与你所说的身份无关。

【讨论】：

所以每当我创建一个 Object 个体时，我都必须断言最后一条语句“hasShape max 0 owl:Thing”，并在创建并关联另一个 Shape 个体时删除该语句？这似乎需要在本体之外创建和管理额外的逻辑。
如果你希望你的本体在 Object 的个体与 Shape 个体没有已知关系时给出不一致，这就是你必须使用 OWL 和 protege 做的事情。否则可能值得考虑使用 RDF 数据存储并使用 SPIN 或 SHACL。不了解您的用例就很难说

【解决方案2】：

我发现的一个解决方案是通过使 owl:Thing 等效于迄今为止定义的所有个体的集合来使本体成为“封闭世界”。

【讨论】：