我正在使用 protege5-5 和推理机 Hermit 1.4 3.456。
我有一个类 Animal 包含 2 个子类 Animal1 和 Animal2。我有一个属性eats 和一个属性isEatenBy，它被定义为eats 的倒数。当我在Animal1 的描述中添加它是eats some(Animal2) 的子类时，我希望推理器在Animal2 的描述中添加它是isEatenBy Animal1 的子类，但事实并非如此。
知道我应该怎么做才能做到这一点，或者我所期望的无论如何都不应该发生？
【问题讨论】：
我认为这里有 3 个问题。
(1) 声明 Animal1 SubClassOf eats some Animal2 仅表明存在 Animal1 集合的个体子集 eats 至少有一个个体属于 Animal2 集合。最多可以推断出Animal2的部分个体被Animal1吃掉了。那就是isEatenBy some Animal1 SubClassOf Animal2。在 (3) 中，我将解释为什么你没有得到这个推断。
最重要的是它不能推断出Animal2 的所有个个体都被Animal1 吃掉了，这是推断Animal2 SubClassOf isEatenBy some Animal1 所需要的。
(2) 反向角色对个人提出主张。因此，当你有一个关于特定个体的陈述，例如eats(animal1, animal2)，其中animal1 和animal2 是个体，推理器会推断出animal2 isEatenBy animal1。
(3) 像isEatenBy some Animal1 这样的类有时被称为匿名类，而像Animal、Animal1 和Animal2 这样的类被称为命名类。因为通常可以从一组公理中得出的推论数量是无限的，所以推理器将他们的推论限制在命名类。
例如，对于您的eats 属性，您可以将域定义为Animal1，将范围定义为Animal2。这意味着，只要您有eats(x, y)，个人x 将被推断为Animal1 类型，而个人y 将被推断为Animal2 类型。
现在还要得到一个等价的推论是isEatenBy some Animal1 SubClassOf Animal2，你需要引入一个新的类，比如AnimalsThatAreEatenByAnimal1，它等价于isEatenBy some Animal1。推理器现在会推断出AnimalsThatAreEatenByAnimal1 是Animal2 的子类。
一般来说，要了解推理者可以做出的推论，了解您定义的公理的语义至关重要。为此，您可以查看direct semantics。逻辑介绍见An Introduction to Description Logics。
【讨论】：