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.