shivajikobardan said:
This is not really a homework question so don't bother answering them.
In contrast, we try to answer questions if and only if they are not homework questions.
Let's introduce the language, or signature.
$L(x, y)$: $x$ likes $y$
$F(x)$: $x$ is food
$E(x,y)$: $x$ eats $y$
$K(x,y)$: $x$ kills $y$
$j$: John
$b$: Bill
$s$: Sue
$a$: apples
$c$: chicken
$p$: peanuts
Now let's write the assumptions and the alleged conclusion. I'll assume that the scope of quantifiers is minimal, e.g., $\forall x\forall y\,F(x)\land F(y)$ is understood as $(\forall x\forall y\,F(x))\land F(y)$ and not as $\forall x\forall y\,(F(x)\land F(y))$.
1. John likes all kinds of food: $\forall x\,(F(x)\to L(j, x))$.
2. Apples are food: $F(a)$.
3. Chicken is food: $F(c)$.
4. Anything anyone eats and isn't killed by is food: $\forall x\,[\exists y\,(E(y, x)\land\neg K(x,y))\to F(x)]$.
5. Bill eats peanuts and is still alive: $E(b,p)\land\neg K(p,b)$.
6. Sue eats everything Bill eats: $\forall x\,(E(b,x)\to E(s,x))$.
Conclusion. John like peanuts: $L(j,p)$.
Perhaps assumption 4 is worth discussing. Why are "anything" and "anyone" written as $\forall$ and $\exists$, respectively? I believe it is because "anything" is at the top level and "anyone" is in the premise of an implication. For example, "Anything is food" is written $\forall x\,F(x)$, but "If anyone eats peanuts, then peanuts are food" means "If there exists a person who eats peanuts, ..." and is written $(\exists x\,E(x, p))\to F(p)$. The latter formula is equivalent to $\forall x\,(E(x,p)\to F(p))$.
Let's convert formulas to prenex form, Skolem normal form and finally to disjuncts.
1. $\forall x\,(F(x)\to L(j, x))\equiv\forall x\,(\neg F(x)\lor L(j, x))\mapsto \neg F(x)\lor L(j, x)$.
2. $F(a)$ is already a disjunct.
3. $F(c)$.
4. $\forall x\,[\exists y\,(E(y, x)\land\neg K(x,y))\to F(x)]\\\equiv\forall x\forall y\,[E(y, x)\land\neg K(x,y)\to F(x)]\\\equiv\forall x\forall y\,[\neg(E(y, x)\land\neg K(x,y))\lor F(x)]\\\equiv\forall x\forall y\,[\neg E(y,x)\lor K(x,y)\lor F(x)]\\\mapsto \neg E(y,x)\lor K(x,y)\lor F(x).$
5. $E(b,p)\land\neg K(p,b)\mapsto E(b,p),\ \neg K(p,b)$.
6. $\forall x\,(E(b,x)\to E(s,x))\equiv\forall x\,(\neg E(b,x)\lor E(s,x))\mapsto \neg E(b,x)\lor E(s,x)$.
Add the negation of conclusion:
7. $\neg L(j,p)$.
Now proceed with resolution derivation.
8. Applying resolution to 1, 7 with substitution $[p/x]$ (i.e., substitution of $p$ for $x$) gives $\neg F(p)$.
9. Applying resolution to 4, 8 with substitution $[p/x]$ gives $\neg E(y,p)\lor K(p,y)$.
10. Applying resolution to the two disjuncts in 5 and to 9 with substitution $[b/y]$ gives first $K(p,b)$ and then the empty disjunct $\Box$.
Thus the negation of the conclusion is refuted and the conclusion itself is proved.
Resolution method is described in more detail in many textbooks, for example, "Logic For Computer Science" by J. Gallier and "A First Course in Logic" by S. Hedman.
