I have been reading on converting first order logic sentences to conjunctive normal form, and then performing resolution.
One of the steps of converting to CNF, is to Standardize variables: rename all variables so that each quantifier has its own unique variable name.
Most general Unifier is the least specialized unification of two clauses.
Question 1: I have been searching to find an example that shows what are the potential problems if I don't standardize variables, but all the online resources I found only explain the "How" and not the "Why". Could you provide me with an example of a potential problem?
Question 2: The same problem as the first question. What if we don't use MGU, and use a more specialized unifier? What are the potential problems? Could you provide me with an example?
My sincere thanks. Felipe