我正在使用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集合中存在至少1个属于Animal2集合的个体子集eats。最多可以推断出一些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的子类。
一般来说，要理解推理者可以做出的推论，理解你定义的公理的语义至关重要。为此，您可以查看直接语义。有关逻辑的介绍，请参阅说明逻辑简介。