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.


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 !


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.