How to learn resolution in predicate logic?

[shivajikobardan]

This is not really a homework question so don't bother answering them. It is more of a guidance problem. This is what I find the hardest out of all topics.. Unfortunately, this topic is a fixed 10 marks question in our 80 marks exam. Comes every time.

The types of questions that I need to deal with my exams are like this-:
john likes all kinds of food.
apples are food
chicken is food
anything anyone eats and isn't killed by is food
bill eats peanuts and is still alive.
sue eats everything bill eats.
prove that john like peanuts using resolution.

 

[Evgeny.Makarov]

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.