I am using protege5-5 and the reasoner HermiT 1.4 3.456.
I have a class Animal containing 2 subclasses Animal1 and Animal2. I have a property eats and a property isEatenBy which is defined as the inverse of eats. When I add in the description of Animal1 that it's subclass of eats some(Animal2), I expect the reasoner to add in the description of Animal2 that it's a subclass of isEatenBy Animal1 but it doesn't.
Any idea what should I do to make that happen or if what I am expecting is not supposed to happen anyway ?
I think there are 3 issues here.
(1) Stating Animal1 SubClassOf eats some Animal2 merely states that there is a subset of individuals of the Animal1 set that eats at least 1 individual that belongs to the set of Animal2. At most you can infer that some individuals of Animal2 are eaten by Animal1. That is that isEatenBy some Animal1 SubClassOf Animal2. In (3) I will explain why you do not get this inference.
Most importantly it cannot infer that all individuals of Animal2 are eaten by Animal1, which is what is needed to infer Animal2 SubClassOf isEatenBy some Animal1.
(2) Inverse roles make claims about individuals. Hence, when you have a statement about specific individuals like eats(animal1, animal2) where animal1 and animal2 are individuals, the reasoner will infer that animal2 isEatenBy animal1.
(3) A class like isEatenBy some Animal1 is sometimes referred to as an anonymous class while classes like Animal, Animal1 and Animal2 are referred to as named classes. Because in general the number of inferences that can be made from a set of axioms is infinite, reasoners restrict their inferences to named classes.
As an example, for your eats property you can define the domain as Animal1 and the range as Animal2. This means that whenever you have eats(x, y), individuals x will be inferred to be of type Animal1 and individual y will be inferred to be of type Animal2.
To now also get an inference that is the equivalent is isEatenBy some Animal1 SubClassOf Animal2, you need to introduce a new class, say AnimalsThatAreEatenByAnimal1 that is equivalent to isEatenBy some Animal1. The reasoner will now infer that AnimalsThatAreEatenByAnimal1 is a subclass of Animal2.
In general, to understand the inferences that a reasoner can make, it crucial to understand the semantics of the axioms you define. For this you can look at the direct semantics. For an introduction on the logic, see An Introduction to Description Logics.