Consider the following axioms- [closed]

Question

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.

Answer 1

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:

9. [3, 6:] $\lnot n(R)$
10. [4, 5:] $w(R) \lor n(R)$
11. [9, 10:] $w(R)$
12. [7, 11:] $\lnot l(G, R)$
13. [2, 3:] $\lnot l(x, S) \lor l(x, R)$
14. [12, 13:] $\lnot l(G, S)$
15. [1, 14:] $\lnot c(G)$
16. [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).