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

Question

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)$ ?

What about the case where:

$\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.

Answer 1

Hey I am currently studying First Order Logic right now and I think I can answer your question. Others please correct me if I am wrong.

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.

Hope this helps !