Choice Between Forward And Backward Chaining

Choice between forward and backward chaining
Forward chaining is often preferable in cases where there are many rules with the same conclusions. A well-known category of such rule systems are taxonomic hierarchies. E.g. the taxonomy of the animal kingdom includes such rules as:
animal(X) :- sponge(X).
animal(X) :- arthopod(X).
animal(X) :- vertebrate(X).
...
vertebrate(X) :- fish(X).
vertebrate(X) :- mammal(X)
...
mammal(X) :- carnivore(X)
...
carnivore(X) :- dog(X).
carnivore(X) :- cat(X).
...
(I have skipped family and genus in the hierarchy.)
Now, suppose we have such a knowledge base of rules, we add the fact "dog(fido)" and we query whether "animal(fido)". In forward chaining, we will successively add "carnivore(fido)", "mammal(fido)", "vertebrate(fido)", and "animal(fido)". The query will then succeed immediately. The total work is proportional to the height of the hierarchy. By contast, if you use backward chaining, the query "~animal(fido)" will unify with the first rule above, and generate the subquery "~sponge(fido)", which will initiate a search for Fido through all the subdivisions of sponges, and so on. Ultimately, it searches the entire taxonomy of animals looking for Fido.
In some cases, it is desirable to combine forward and backward chaining. For example, suppose we augment the above animal with features of these various categories:
breathes(X) :- animal(X).
...
backbone(X) :- vertebrate(X).
has(X,brain) :- vertebrate(X).
...
furry(X) :- mammal(X).
warm_blooded(X) :- mammal(X).
...
If all these rules are implemented as forward chaining, then as soon as we state that Fido is a dog, we have to add all his known properties to Gamma; that he breathes, is warm-blooded, has a liver and kidney, and so on. The solution is to mark these property rules as backward chaining and mark the hierarchy rules as forward chaining. You then implement the knowledge base with both the forward chaining algorithm, restricted to rules marked as forward chaining, and backward chaining rules, restricted to rules marked as backward chaining. However, it is hard to guarantee that such a mixed inference system will be complete.