I have to find the Most General Unifier of the following atomic sentences
P(x1,G(x2,x3),x2,B) and P(G(H(A,x5),x2),x1,H(A,x4),x4)
After using the Martelli-Montanari Algorithm I ended up on the following MGU:
[G(H(A,B),H(A,B))/x1 , B/x5 , H(A,B)/x3 , H(A,B)/x2 , B/x4]
I noticed that both x2 and x3 have the same function. Does that make my MGU valid or there is no MGU for the above sentences ? I don't think i have done anything wrong , while executing my algorithm.
(Detailed steps can be provided if asked)
If you start with the original forms and do the substitutions on them, you substitute H(A, B) for x3 and H(A, B) for x2. The expression H(A, B) is well-formed in both cases and well-formedness makes for the only requirement to substitute an expression for a variable. So, no having the same expression for different variables is not a problem (note authors generally seem to say that H is the function and H(A, B) is the expression).
I'll note that the unification algorithm only fails when the occurs check happens or we have symbol clash.
Perhaps to review, symbol clash happens when we have a functional symbol not matching another functional symbol when they have the same position in the formula and we have unification up to that position in the formula. For example, if we tried to unify F(a, b) and G(a, b), then F and G clash. As another example, assuming all small letters as variables, if we try to unify F(a, G(b, c)) with F(H(i, j), K(l, m)), then we have K and G clashing, so symbol clash occurs.
The occurs check happens when we would have to unify a variable with an expression which also contains that variable (the impossibility of this basically got noted before unification even existed as a well-developed concept in a paper on the equivalential calculus by Lukasiewicz, if I recall correctly talking about how no thing can be congruent with one of it's proper parts). For example, if we tried to unify F(x, G(b, c)) and F(H(x, b), G(b, c)), then the occurs check happens, since if we substitute x with H(x, b) in both expressions we have H(x, b) in one and H(H(x, b), b) in another. Then we would need to substitute x with H(x, b) in both expressions. And so on with a recursion that never halts.
Now, working through your substitutions we have
G(H(A, B), H(A, B)) as the first part of the first clause
and
G(H(A, B), H(A, B)) for the first part of the second clause
so that looks good.
But for the second parts we have
H(A, B)
and
G(H(A, B), H(A, B))
So, we have symbol clash here, and thus what you've proposed is not a unifier.