Comments on Unification

Source: Maria Gini, University of Minnesota (recommended by Tyler Bienhoff)

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