Forward Chaining First Order Logic (Unification)

Question

I'm studying for my final exam and I'm having trouble understanding this FC algorithm:

I understand it up to the part where you standardize each rule. Then I think the next line is saying for each theta that satisfied the Generalized Modus Ponens (p'_iTheta = p_iTheta), do... something. What is that something? I don't really understand what is happening after that part.

Any help is appreciated. Thanks for reading.

Answer 1

Basically, Theta is a substitution that can make some set of terms you know to be true (the p's in the KB) equal to the ps in the rule, then you can conclude that q' (q with the same Theta applied to it) is also true. If that q' isn't already known, then it goes into new; if it unifies w/ our query, then we've succeeded.