Most General Unification in Prolog-EBG algorithm

I am reading the algorithm of prolog-EBG in Machine Learning by Tom Mitchell, and the following algorithm has a step to compute a most general unification:

$$\theta_{hl}:$$ the most general unifier of $$head$$ with $$Literal$$ such that there exists a substitution $$\theta_{li}$$ for which: $$\theta_{li} (\theta_{hl} (head))= \theta_{hi}(head)$$

Here head means the head of a rule, Literal is a selected literal. In the example given:

$$head=Weight (z,5)$$ $$Literal = Weight(y,wy)$$ $$\theta_{hi} = \{z/Obj_2\}$$ $$\theta_{hl}= \{z/y, wy/5\}, where\ \theta_{li} = \{y/Obj2\}$$

Here the book states that:

The notation {z/y} denotes the substitution of y in place of z.

I am doing this unification on my own following Martelli, Montanari's algorithm and I feel quite confused.

$$\{Weight(y,wy)/ Weight(z,5)\}$$:

Since weight is the same predicate with same arity 2, do $$\{z/y, 5/wy \}$$.

Then I find confused at:

1. Which is the Variable, z, y, wy?
2. How to unify when we have constants here?
• It is not "propositional calculus". – Mauro ALLEGRANZA Jun 12 at 13:33

Comment : a substitution $$\theta = \{ v_1/t_1,\ldots,v_n/t_n \ \}$$ acts on an expression $$E$$ and $$\theta(E)$$ is the expression obtained from $$E$$ by replacing simultaneously each occurrence of the variable $$v_i$$ with term $$t_i$$.

Thus, if we assume that $$\text {Weight}(z,5)$$ is an atomic formula (or literal) expressing the fact that the Weight of $$z$$ is $$5$$, it is not a term and we have to apply substitutions to it.

Having said that, using the substitutions defined above we have :

$$θ_{hi} (\text {head}) = θ_{hi} (\text {Weight}(z,5)) = \text {Weight}(\text {Obj}_2,5)$$.

And : $$θ_{hl} (\text {head}) = \text {Weight}(y,5)$$.

Thus,

$$θ_{li} (θ_{hl} (\text {head})) = θ_{li} (\text {Weight} (y,5)) = \text {Weight} (\text {Obj}_2 ,5)$$.

Conclusion :

$$θ_{li} (θ_{hl} (\text {head})) = θ_{hi} (\text {head})$$.

If instead we want to unify $$\text {head}$$ with $$\text {Literal}$$, what we need is to apply the substitution $$θ_{hl}$$ to both to get :

$$\text {Weight} (y,5)$$.