不推论一个性质的逆子类

Question

我使用的是蛋白酶5-5和推理者HermiT 1.4 3.456.

我有一个类Animal，包含两个子类Animal1和Animal2。我有一个属性eats和一个属性isEatenBy，它被定义为eats的反义词。当我添加Animal1的描述(它是eats some(Animal2)的子类)时，我希望推理者添加Animal2的描述，说明它是isEatenBy Animal1的子类，但它没有。

你知道我该怎么做才能让这一切发生，或者我所期待的一切都不应该发生吗？

Answer 1

我想这里有三个问题。

(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的一个子类。

一般来说，要理解推理者可以做出的推论，关键是要理解您定义的公理的语义。为此，您可以查看直接语义学。有关逻辑的介绍，请参见描述逻辑概论。