MHB How to learn resolution in predicate logic?

Click For Summary
Learning resolution in predicate logic is crucial for tackling fixed exam questions, particularly those involving complex relationships like preferences for food. The discussion outlines a specific example involving John, Bill, and Sue, demonstrating how to express statements using logical formulas. Key steps include converting assumptions to prenex and Skolem normal forms, and applying resolution to derive the conclusion that John likes peanuts. The importance of understanding quantifiers and their implications in logical statements is emphasized. Mastery of these concepts is essential for success in exams focused on predicate logic.
shivajikobardan
Messages
637
Reaction score
54
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.
 
Technology news on Phys.org
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.
 
Learn If you want to write code for Python Machine learning, AI Statistics/data analysis Scientific research Web application servers Some microcontrollers JavaScript/Node JS/TypeScript Web sites Web application servers C# Games (Unity) Consumer applications (Windows) Business applications C++ Games (Unreal Engine) Operating systems, device drivers Microcontrollers/embedded systems Consumer applications (Linux) Some more tips: Do not learn C++ (or any other dialect of C) as a...

Similar threads

  • · Replies 2 ·
Replies
2
Views
2K
Replies
1
Views
3K
  • · Replies 36 ·
2
Replies
36
Views
10K
Replies
6
Views
4K
  • · Replies 5 ·
Replies
5
Views
4K
  • · Replies 7 ·
Replies
7
Views
3K
  • · Replies 7 ·
Replies
7
Views
4K
  • · Replies 3 ·
Replies
3
Views
4K
  • · Replies 31 ·
2
Replies
31
Views
5K