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.

enter description here


1 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:

  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).


Not the answer you're looking for? Browse other questions tagged .