# Consider the following axioms- [closed]

I'm studying Artificial Intelligence and I have a question about first order logic and resolution. But I couldn't find any answer why.

I tried using Google to get the answer but nothing was found.

For first part it's extremely straightforward to encode each axiom into FOL wff's as knowledge base:

1. $$\forall x (c(x) \to l(x, S)$$
2. $$\forall x (l(x, S) \to \forall y (d(y) \to l(x, y)))$$
3. $$d(R) ∧ r(R)$$
4. $$\forall x (r(x) → w(x) ∨ n(x))$$
5. $$¬ ∃ x (d(x) ∧ n(x))$$
6. $$∀ x (w(x) → ¬ l(G, x))$$
7. $$¬ c(G)$$ (to be proved)

where $$c$$:=child, $$l$$=loves, $$d$$:=reindeer, $$r$$:=rednose, $$w$$:=weird, $$n$$:=clown, $$S$$:=Santa, $$R$$:=Rudolph, $$G$$:=Scrooge, respectively, in the meta language.

Then convert them to definite, unit and goal clauses via Skolemization:

1. $$\lnot c(x) \lor l(x, S)$$
2. $$\lnot l(x, S) \lor \lnot d(y) \lor l(x, y)$$
3. $$d(R)$$
4. $$r(R)$$
5. $$\lnot r(x) \lor w(x) \lor n(x)$$
6. $$\lnot d(x) \lor \lnot n(x)$$
7. $$\lnot w(x) \lor \lnot l(G, x)$$
8. $$c(G)$$ (goal clause)

From here we can further resolve clauses:

1. [3, 6:] $$\lnot n(R)$$
2. [4, 5:] $$w(R) \lor n(R)$$
3. [9, 10:] $$w(R)$$
4. [7, 11:] $$\lnot l(G, R)$$
5. [2, 3:] $$\lnot l(x, S) \lor l(x, R)$$
6. [12, 13:] $$\lnot l(G, S)$$
7. [1, 14:] $$\lnot c(G)$$
8. [15, 8:] $$\bot$$ Q.E.D.

Finally note that not any arbitrary contradictory set of clauses can be derived by resolution inference rule such as the simple case where $$p \lor q$$ cannot be derived from $$\Gamma = \{p\}$$ by resolution, though the classical FOL is semantically complete per Gödel's completeness theorem and thus the formal system with all inference rules of FOL containing the axiom set $$\Gamma$$ is strongly and refutation complete (but not necessarily negation complete due to the renowned Gödel's incompleteness theorems).