Use Resolution to proove a sentence in First Order Logic

Question

I was just wondering if anyone could tell me if I've solved this problem right. If wrong, I would like to know what I did wrong.

"Use resolution to prove Green(Linn) given the information below. You must first convert each sentence into CNF. Feel free to show only the applications of the resolution rule that lead to the desired conclusion. For each application of the resolution rule, show the unification bindings, θ."

I have this axioms to start with:

• Hybrid(Prius)
• Drives(Linn, Prius)
• ∀x Green(x) <--> Bikes(x) ∨ (∃y Drives(x, y) ∧ Hybrid(y))

So this is my attempt to solve it. I won't write everything because it's a lot, but my results for each step.

I need to turn every axiom into CNF. The first and the second is already in CNF, so I need to turn the third axiom to CNF.

1. I start with removing the biconditional.
   (∀x Green(x) --> Bikes(x) ∨ (∃y Drives(x, y) ∧ Hybrid(y))) ∧
   ((Bikes(x) ∨ (∃y Drives(x, y) ∧ Hybrid(y))) --> Green(x))

2. Next step is to remove the implications.
   (∀x ¬Green(x) ∨ Bikes(x) ∨ (∃y Drives(x, y) ∧ Hybrid(y))) ∧
   (¬(Bikes(x) ∨ (∃y Drives(x, y) ∧ Hybrid(y)) ∨ Green(x))

3. Move the ¬ inwards.
   (∀x ¬Green(x) ∨ Bikes(x) ∨ (∃y Drives(x, y) ∧ Hybrid(y))) ∧
   ((¬Bikes(x) ∧ (∀y ¬Drives(x, y) ∨ ¬Hybrid(y)) ∨ Green(x))

4. Skolemize the exitensial variable with a Skolem constant/function.
   (∀x ¬Green(x) ∨ Bikes(x) ∨ Drives(x, A) ∧ Hybrid(A))) ∧
   ((¬Bikes(x) ∧ (∀y ¬Drives(x, y) ∨ ¬Hybrid(y)) ∨ Green(x))

5. Remove the universal quantifier.
   (¬Green(x) ∨ Bikes(x) ∨ (Drives(x, A) ∧ Hybrid(A)))) ∧
   ((¬Bikes(x) ∧ (¬Drives(x, y) ∨ ¬Hybrid(y)) ∨ Green(x))

6. Distribute ∧ over ∨
   (¬Green(x) ∨ Bikes(x) ∨ Drives(x, A)) ∧ (¬Green(x) ∨ Bikes(x) ∨ Hybrid(A)) ∧
   (¬Bikes(x) ∨ Green(x)) ∧ (¬Drives(x, y) ∨ ¬Hybrid(y) ∨ Green(x))

Result: I end up with these 6 sentences I can use for the resoultion proof.
1. ¬Green(x) ∨ Bikes(x) ∨ Drives(x, A)
2. ¬Green(x) ∨ Bikes(x) ∨ Hybrid(A)
3. ¬Bikes(x) ∨ Green(x)
4. ¬Drives(x, y) ∨ ¬Hybrid(y) ∨ Green(x)
5. Hybrid(Prius)
6. Drives(Linn, Prius)

So my proof.
7. ¬Drives(x, Prius) ∨ Green(x) // I resolve 4 and 6. {y/Prius}
8. Green(Linn) // I resolve 6 and 7. {x/Linn}

This is it. I am not sure whether I've done it right or not. My proof is only two steps where I mostly resolve/merge some of the sentences. Can I do this?

Also, in my CNF steps, I'm not sure in step two, whether it should be ∀x ¬Green(x) or ∃x ¬Green(x) (Because ¬( ∀x Green(x) ), or can I move the negation directly in front of Green(x)?

I'd really appreciate any feedback. I'm pretty sure my attempt is not right.

Thanks in advance!

Answer 1

Your step 2 is correct if we read :

$∀xGreen(x) \leftrightarrow Bikes(x) \lor (∃y Drives(x, y) \land Hybrid(y))$

as :

$∀x[Green(x) \leftrightarrow (Bikes(x) \lor ∃y (Drives(x, y) \land Hybrid(y)))]$.

In this case, removing the conditional we get :

$∀x[(\lnot Green(x) \lor Bikes(x) \lor ∃y (Drives(x, y) \land Hybrid(y))) \land (\lnot (Bikes(x) \lor ∃y (Drives(x, y) \land Hybrid(y))) \lor Green(x))].$

---

Regarding the resolution proof, it must work, because, from :

1) $Hybrid(Prius)$

2) $Drives(Linn, Prius)$

3) $∀x[(Bikes(x) \lor ∃y (Drives(x, y) \land Hybrid(y))) \rightarrow Green(x)]$

i.e. using only "half" of the bi-conditional, we have :

4) $(Bikes(Linn) \lor ∃y (Drives(Linn, y) \land Hybrid(y))) \rightarrow Green(Linn)$ --- from 3) $\forall$-elimination, i.e. instantiating the universal quantifier with $x = Linn$

5) $Drives(Linn, Prius) \land Hybrid(Prius)$ --- from 1) and 2) by $\land$-introduction

6) $\exists y (Drives(Linn, y) \land Hybrid(y))$ --- from 5) by $\exists$-introduction

7) $Bikes(Linn) \lor (\exists y (Drives(Linn, y) \land Hybrid(y)))$ --- from 6) by $\lor$-introduction

8) $Green(Linn)$ --- from 7) and 4) by $\rightarrow$-elimination (modus ponens)

---

Regarding resolution, in order to prove that from the three axioms it follows $Green(Linn)$, we have to add to the six clauses also : 7. $\lnot Green(Linn)$ [because : $\Gamma \vDash \varphi$ iff $\Gamma \cup \{ \lnot \varphi \}$ is unsatisfiable].

With it, it is easy to derive the empty clause $\square$ from 4-7.