With the help of resolution graph, resolution in FOL, solve the following things:

Adding the negation "John does not like peanuts" to the knowledge base and resolving leads to the empty clause, so "John likes peanuts" is proved.

Step 1: FOL sentences (f and g are the background facts that link "alive" and "not killed"):

1. \(\forall x\ \mathrm{food}(x) \rightarrow \mathrm{likes}(John, x)\)
2. \(\mathrm{food}(Apple) \wedge \mathrm{food}(Vegetables)\)
3. \(\forall x\forall y\ \mathrm{eats}(x,y) \wedge \neg\mathrm{killed}(x) \rightarrow \mathrm{food}(y)\)
4. \(\mathrm{eats}(Bill, Peanuts) \wedge \mathrm{alive}(Bill)\)
5. \(\forall x\ \mathrm{eats}(Bill, x) \rightarrow \mathrm{eats}(Julie, x)\)
6. \(\forall x\ \neg\mathrm{killed}(x) \rightarrow \mathrm{alive}(x)\)
7. \(\forall x\ \mathrm{alive}(x) \rightarrow \neg\mathrm{killed}(x)\)

Goal: \(\mathrm{likes}(John, Peanuts)\).

Step 2: Clause (CNF) form (remove implications, standardise variables, drop \(\forall\)):

1. \(\neg\mathrm{food}(x) \vee \mathrm{likes}(John, x)\)
2. \(\mathrm{food}(Apple)\)
3. \(\mathrm{food}(Vegetables)\)
4. \(\neg\mathrm{eats}(y,z) \vee \mathrm{killed}(y) \vee \mathrm{food}(z)\)
5. \(\mathrm{eats}(Bill, Peanuts)\)
6. \(\mathrm{alive}(Bill)\)
7. \(\neg\mathrm{eats}(Bill, w) \vee \mathrm{eats}(Julie, w)\)
8. \(\mathrm{killed}(g) \vee \mathrm{alive}(g)\)
9. \(\neg\mathrm{alive}(k) \vee \neg\mathrm{killed}(k)\)
10. Negated goal: \(\neg\mathrm{likes}(John, Peanuts)\)

Step 3: Resolution

• (10) + (1), \(\{x/Peanuts\}\): \(\neg\mathrm{food}(Peanuts)\)
• + (4), \(\{z/Peanuts\}\): \(\neg\mathrm{eats}(y, Peanuts) \vee \mathrm{killed}(y)\)
• + (5), \(\{y/Bill\}\): \(\mathrm{killed}(Bill)\)
• + (9), \(\{k/Bill\}\): \(\neg\mathrm{alive}(Bill)\)
• + (6): empty clause \(\square\)

Resolution graph (each step resolves the line above with the clause shown):

¬likes(John,Peanuts)   ¬food(x) ∨ likes(John,x)
            \            /   {x/Peanuts}
         ¬food(Peanuts)    ¬eats(y,z) ∨ killed(y) ∨ food(z)
                    \        /   {z/Peanuts}
      ¬eats(y,Peanuts) ∨ killed(y)    eats(Bill,Peanuts)
                         \             /   {y/Bill}
                        killed(Bill)    ¬alive(k) ∨ ¬killed(k)
                              \          /   {k/Bill}
                           ¬alive(Bill)    alive(Bill)
                                  \          /
                                  { } (empty)

The contradiction shows the negated goal is false, so John likes peanuts. (Clauses 2, 3, 7 and 8 were not needed for this proof.)