# Does the substituted variable/constant have to appear in the unified term?

I'm checking out how to manually apply resolution on a first order predicate logic knowledge base and I'm confused about what is allowed or not in the algorithm.

Let's say that we have the following two clauses (where $$A$$ and $$B$$ are constants):

$$\neg P(A, B) \vee H(A)$$

$$\neg L(x_1) \vee P(x_1, y_1)$$

If I try to unify these two clauses by making the substitutions $$\{x_1/A, y_1/B\}$$ do I get $$\neg L(A) \vee H(A)$$ ? Is it allowed to substitute $$y_1$$ by $$B$$ even if $$B$$ doesn't appear in the unified clause?

Then we have the other way around where:

$$\neg P(A, y_1) \vee H(A)$$

$$\neg L(x_1) \vee P(x_1, B)$$

Can I do $$\{x_1/A, B/y_1\}$$ for $$\neg L(A) \vee H(A)$$ ?

$$\neg P(A, z_1) \vee H(A)$$

$$\neg L(x_1) \vee P(x_1, y_1)$$

Can I substitute $$\{x_1/A, y_1/z_1\}$$ and get $$\neg L(A) \vee H(A)$$ ?

Finally there is also the cases where we have something like this:

$$\neg P(x_2, y_2) \vee H(z_1)$$

$$\neg L(x_1) \vee P(x_1, y_1)$$

Can we do $$\{x_1/x_2, y_1/y_2\}$$ to get $$\neg L(x_3) \vee H(z_2)$$ ?

I'm really confused about when unification succeeds once we have two clauses with a literal of the same kind (negation in one of them and not in the other one) that are a candidates for unification.

For the first case, you can generally substitute variables with constants. Hence, you can make the substitution $$\theta \leftarrow \{x_1 \leftarrow A, y_1 \leftarrow B \}$$. This is used very commonly when you want to infer some query $$\alpha$$ from your knowledge base. $$\alpha$$ usually is in the form $$P(A,B)$$ as you have mentioned. When you unify you get $$\neg L(A) \vee H(A)$$ and ur substitution has to stay the same throughout the resolution algorithm. I.e, you cannot substitute $$x_1$$ for another constant / variable.
Regarding the second case, you cannot substitute a constant with a variable $$B$$ to another variable.
In general, you can substitute a variable with a constant, or another variable. You can also substitute a variable with a skolem function, Eg. $$x_1 \leftarrow G(y)$$. However, for skolem functions, you cannot substitute $$x \leftarrow F(x)$$, in which the variable names are the same.