Most General Unifier(MGU)

Most General Unifier
Least specialized unification of two clauses.
We can compute the MGU using the disagreement set
Dk = {e1, e2}: the pair of expressions where two clauses first
disagree.
REPEAT UNTIL no more disagreement → found MGU.
IF either e1 or e2 is a variable V and the other is some term (or a
variable) t, then choose V = t as substitution.
Then substitute to obtain Sk+1 and find disagreement set Dk+1.
ELSE unification is not possible.
MGU - Example 1
Find the MGU of p(f (a), g(X)) and p(Y ,Y ):
S0 = {p(f (a), g(X)) ; p(Y ,Y )}
 D0 = {f (a),Y }
 σ = {Y = f (a)}
 S1 = {p(f (a), g(X)) ; p(f (a), f (a))}
 D1 = {g(X), f (a)}
 no unification possible!
MGU - Example 2
 S0 = {p(a,X, h(g(Z))) ; p(Z, h(Y ), h(Y ))}
 D0 = {a, Z}
 σ = {Z = a}
 S1 = {p(a,X, h(g(a))) ; p(a, h(Y ), h(Y ))}
 D1 = {X, h(Y )}
 σ = {Z = a,X = h(Y )}
 S2 = {p(a, h(Y ), h(g(a))) ; p(a, h(Y ), h(Y ))}
 D2 = {g(a),Y }
 σ = {Z = a,X = h(Y ),Y = g(a)}
 S3 = {p(a, h(g(a)), h(g(a))) ; p(a, h(g(a)), h(g(a)))}
 No disagreement
⇒ σ = {Z = a,X = h(Y ),Y = g(a)} is MGU
MGU - Example 3
 S0 = {p(X,X) ; p(Y , f (Y ))}
 D0 = {X,Y }
 σ = {X = Y }
 S1 = {p(Y ,Y ) ; p(Y , f (Y ))}
 D1 = {Y , f (Y )}
 no unification possible!