One way of looking at this question is work in termination analysis of logic programs (googling "termination analysis of logic programs" isn't a bad way to find some of the relevant research.)
As an example, if the rules I am looking at look like this:
lt(zero,succ(Y)).
lt(succ(X),succ(Y)) <= lt(X,Y).
I know that resolution will succeed or finitely fail for any query ?lt(n,X) where n is a ground term, because every subgoal that arises will have a smaller first argument than the subgoal that led to its generation. On the other hand, if the rules I am looking at look like this:
path(X,Z) <= path(X,Y), path(Y,Z).
I know that, given a n path(,) facts, I can only derive at most a finite number of other path(,) facts (on the order of n2, in fact), which ensures that saturation will terminate (assuming what I think of as saturation is what you think of as Gilmore's saturation).
(A deeper investigation of where the difference between these methods comes from, can be found in Chaudhuri, Pfenning, and Price, A Logical Characterization of Forward and Backward Chaining in the Inverse Method. Journal of Automated Reasoning, 40(2–3), pp. 133–177. 2008., but the response above seemed more relevant to the question.)
