使用 Pellet 和 HermiT 了解 Protege 中的通用量化答案

【问题标题】：Understanding Universal Quantification in Protege with Pellet and HermiT使用 Pellet 和 HermiT 了解 Protege 中的通用量化
【发布时间】：2016-10-07 13:06:15
【问题描述】：

我是 Protégé 的新手，所以我有一个非常基本的问题。我有课程Child 和Parent。 Child 有子类Girl。

child1 的类型为 Girl，child2 的类型为 Child，anna 和 peter 的类型均为 Parent。此外，还有关系anna isParentOf child1和peter isParentOf child2，没有进一步的特征。

现在我想定义类ParentOfGirl，使其等价于Parent and isParentOf only Girl。我希望推理器推断anna 具有这种新类型，但它没有。

我将Inverse functional 属性添加到isParentOf，因为父母可以有多个孩子。如果我再将Symmetric 添加到关系中，我得到anna 的类型为ParentOfGirl，但我不希望isParentOf 是对称的。

如果我看一下上面没有对称的语义，我会看到：

ParentOfGirl ≡ {anna, peter} ⋂ { x ∊ owl:Thing |如果 ∀y (x, y) ∊ isParentOf 那么 y ∊ 女孩}

child1 ∊ 孩子和 child1 ∊ 女孩

isParentOf ≡ {(anna, child1), (peter, child2)}

那么child1 是与anna 相关的唯一Child 类型的个体，它也具有Girl 类型。在我看来，在这种情况下，推理器只能从右到左查看关系，因为如果isParentOf 是对称的，它会推导出anna。此外，如果peter 与 child2 无关，我希望它也会在ParentOfGirl 中。但这也不会发生。

为什么推理器（Pellet 或 HermiT）看不到 anna 是 ParentOfGirl？

【问题讨论】：

OWL 遵循开放世界假设 (OWA)，即在您的本体中，anna 可能是另一个不是女孩的孩子的父母。推理器也遵循此 OWA，无法推断 anna 的类型为 ParentOfGirl
另外，对我来说，你的本体的语义还不清楚。为什么你认为isParentOf 适合做反函数？
我希望 OWA 不会改变任何东西。如果我们有一个知识库 KB = {PO(a,p)} 并且我想从 KB α = ∀x.POG(x, p) 推断，我会得到 True，因为 KB 的所有解释都满足 α。为什么isParentOf和PO的定义不一样？
在我看来，关系是否是反向函数对我的问题并不重要。语义不表示关系的任何类型的特征。但它不会与反向功能相矛盾。
“OWA 不会改变任何东西”——我不知道那是什么意思。正如我所说，你不能推断出这一点，因为 OWL 和任何 OWL 推理器都遵循开放世界假设，即不知道的事实不被假设为 FALSE，这将在封闭世界假设下发生，例如在数据库中。这意味着anna 可能是另一个孩子的父母，只是不知道。

标签： logic owl protege reasoning pellet

【解决方案1】：

@AKSW 在评论中是正确的。推理者无法判断父母是否只有女孩。您需要声明此功能，例如通过向个人添加类型。

在这种情况下，此断言将等同于您寻求的推理 - 所以它不是一个很好的解决方法。

如果您将 forall 更改为一些，您将能够找到至少一个女孩的父母。这是您的目标类的超类，可能会帮助您的应用程序。

【讨论】：

必须给个体添加什么样的类型才能获得这种推断？是否有用于在 Protégé 或类似的东西中设置封闭世界假设的全局标志，还是没有意义？
这是一个推理级别设置。 Pellet 支持它，但我不确定其他推理者支持它。