# Comments on unification

Here is a synopsis of how the unification algorithm works on different combinations of arguments. The rows in the table indicate the arguments for one predicate, the columns indicate the arguments for the other. The notation (x/y) indicates that x is substituted by y.

 constant variable function constant SUCCESS if constants are the same, FAIL otherwise {variable/constant} FAIL variable {variable/constant} {variable/variable} {variable/function} if variable does not occur in function, FAIL otherwise function FAIL {variable/function} if variable does not occur in function, FAIL otherwise the result of unifying the arguments if the functions are the same and the arguments unify, FAIL otherwise

### Examples

In the following examples we are interested just in unification, not in resolution.
• P(x) unifies with P(A) using the substitution {x/A}
• P(f(x), y, g(y)) unifies with P(f(w), z, g(A)) using the substitutions {x/w, y/z, z/A}
• P(f(x), y, g(y)) fails to unify with P(f(w), B, g(A)) since y is unified with B and so it cannot be unified with A
• P(f(x), y, g(y)) fails to unify with P(f(w), f(A), g(A)) since y is unified with f(A) and so it cannot be unified with A