Answers.Body: <p>For first part it's extremely straightforward to encode each axiom into FOL wff's as knowledge base:</p>
  <ol>
  <li><span class="math-container">$\forall x (c(x) \to l(x, S)$</span></li>
  <li><span class="math-container">$\forall x (l(x, S) \to \forall y (d(y) \to l(x, y)))$</span></li>
  <li><span class="math-container">$d(R) ∧ r(R)$</span></li>
  <li><span class="math-container">$\forall x (r(x) → w(x) ∨ n(x))$</span></li>
  <li><span class="math-container">$¬ ∃ x (d(x) ∧ n(x))$</span></li>
  <li><span class="math-container">$∀ x (w(x) → ¬ l(G, x))$</span></li>
  <li><span class="math-container">$¬ c(G)$</span> (to be proved)</li>
  </ol>
  <p>where <span class="math-container">$c$</span>:=child, <span class="math-container">$l$</span>=loves, <span class="math-container">$d$</span>:=reindeer, <span class="math-container">$r$</span>:=rednose, <span class="math-container">$w$</span>:=weird, <span class="math-container">$n$</span>:=clown, <span class="math-container">$S$</span>:=Santa, <span class="math-container">$R$</span>:=Rudolph, <span class="math-container">$G$</span>:=Scrooge, respectively, in the meta language.</p>
  <p>Then convert them to definite, unit and goal clauses via Skolemization:</p>
  <ol>
  <li><span class="math-container">$\lnot c(x) \lor l(x, S)$</span></li>
  <li><span class="math-container">$\lnot l(x, S) \lor \lnot d(y) \lor l(x, y)$</span></li>
  <li><span class="math-container">$d(R)$</span></li>
  <li><span class="math-container">$r(R)$</span></li>
  <li><span class="math-container">$\lnot r(x) \lor w(x) \lor n(x)$</span></li>
  <li><span class="math-container">$\lnot d(x) \lor \lnot n(x)$</span></li>
  <li><span class="math-container">$\lnot w(x) \lor \lnot l(G, x)$</span></li>
  <li><span class="math-container">$c(G)$</span> (goal clause)</li>
  </ol>
  <p>From here we can further resolve clauses:</p>
  <ol start="9">
  <li>[3, 6:] <span class="math-container">$\lnot n(R)$</span></li>
  <li>[4, 5:] <span class="math-container">$w(R) \lor n(R)$</span></li>
  <li>[9, 10:] <span class="math-container">$w(R)$</span></li>
  <li>[7, 11:] <span class="math-container">$\lnot l(G, R)$</span></li>
  <li>[2, 3:] <span class="math-container">$\lnot l(x, S) \lor l(x, R)$</span></li>
  <li>[12, 13:] <span class="math-container">$\lnot l(G, S)$</span></li>
  <li>[1, 14:] <span class="math-container">$\lnot c(G)$</span></li>
  <li>[15, 8:] <span class="math-container">$\bot$</span> Q.E.D.</li>
  </ol>
  <p>Finally note that not any arbitrary contradictory set of clauses can be derived by resolution inference rule such as the simple case where <span class="math-container">$p \lor q$</span> cannot be derived from <span class="math-container">$\Gamma = \{p\}$</span> by resolution, though the classical FOL is <em>semantically complete</em> per Gödel's <a href="https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem#" rel="nofollow noreferrer">completeness theorem</a> and thus the  formal system with all inference rules of FOL containing the axiom set <span class="math-container">$\Gamma$</span> is <em>strongly and refutation complete</em> (but not necessarily <em>negation complete</em> due to the renowned <a href="https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems" rel="nofollow noreferrer">Gödel's incompleteness theorems</a>).</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2022-11-23T23:43:16.337Z
Answers.LastActivityDate: 2022-11-24T00:46:28.660Z
Answers.LastEditDate: 2022-11-24T00:46:28.660Z
Answers.UserDisplayName: cinch
Body: <p>I'm studying Artificial Intelligence and I have a question about first order logic and resolution. But I couldn't find any answer why.</p>
  <p>I tried using Google to get the answer but nothing was found.</p>
  <p><a href="https://i.sstatic.net/hyhXI.jpg" rel="nofollow noreferrer"><img src="https://i.sstatic.net/hyhXI.jpg" alt="enter description here" /></a></p>
  
Tags: <logic><superintelligence>
Title: Consider the following axioms-
UserDisplayName: Sadman
ThreadText: # Consider the following axioms-
  
  (Asked by: username_0 on 2022-11-18)
  
  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](https://i.sstatic.net/hyhXI.jpg)](https://i.sstatic.net/hyhXI.jpg)
  
  **Tags:** logic, superintelligence
  
  
  ---
  
  ## 1 answers
  
  ### Answer by username_1 on 2022-11-23. Score: 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](https://en.wikipedia.org/wiki/G%C3%B6del%27s_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](https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems)).
  
  
  ---
  
  