# Most General unifier in logic

i have a question about most general unifier in logic. i'll begin by saying that in the class we were only given a summary in a few words, without any example, and they just moved on to the next topic and left us wondering on how to solve it, so i am trying based on what i've learnt from reading here:

i need to find the MGU, if it exists, for every pair of atomic propositions.

1)$$Q(one, two, two)$$ , $$Q(x,y,z)$$

2)$$R(x,F(A,B)$$ , $$R(F(y,y),x)$$

my attempt:

1)not exist because Two is written twice and we can't use substitution so that it will have two different meanings.

2)$$R(F(x,B), F(A,B)), R(F(y,y),F(x,B))$$

is it correct? would really appreciate your assistance and correction with this. thank you very much

• See this post for the def of unifier. – Mauro ALLEGRANZA Apr 18 at 7:36
• The subst : $x \leftarrow \text {one}, y \leftarrow \text {two}, z \leftarrow \text {two}$ will work. – Mauro ALLEGRANZA Apr 18 at 7:37
• and for the second? meanwhile i am trying to find also explanations on youtube and worked examples to learn how to apply the theory correctly – hps13 Apr 18 at 7:58
• Similar; see the def in the linked post. A subst is an operation of replacing terms in place of variables. Thus, start with $A$ and $B$ in place of $y$. – Mauro ALLEGRANZA Apr 18 at 8:13
• @MauroALLEGRANZA the second should be $/theta = [F(y,y)/x, a/x,b/x]$ ? – hps13 Apr 22 at 11:55