How to learn resolution in predicate logic?

Click For Summary
SUMMARY

The discussion focuses on mastering the resolution method in predicate logic, specifically for proving statements in exam scenarios. The example provided illustrates how to derive the conclusion that "John likes peanuts" using logical formulas and resolution steps. Key assumptions include the definitions of food and eating relationships, which are expressed through predicates such as $L(x, y)$ for "likes" and $E(x, y)$ for "eats." The resolution process is detailed, culminating in the refutation of the negation of the conclusion, thereby confirming its validity.

PREREQUISITES
  • Understanding of predicate logic and quantifiers
  • Familiarity with resolution methods in logic
  • Knowledge of logical formulas and their transformations
  • Basic concepts of Skolem normal form and prenex form
NEXT STEPS
  • Study the resolution method in depth using "Logic For Computer Science" by J. Gallier
  • Explore Skolemization and its applications in predicate logic
  • Learn about converting logical formulas to prenex form
  • Practice deriving conclusions using resolution with various examples
USEFUL FOR

Students preparing for exams in logic, educators teaching predicate logic, and anyone interested in enhancing their skills in formal reasoning and proof techniques.

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.
 

Similar threads

  • · Replies 2 ·
Replies
2
Views
2K
  • · Replies 3 ·
Replies
3
Views
2K
  • · Replies 23 ·
Replies
23
Views
5K
  • · Replies 2 ·
Replies
2
Views
3K
  • · Replies 54 ·
2
Replies
54
Views
8K
Replies
15
Views
4K
  • · Replies 28 ·
Replies
28
Views
10K
  • · Replies 36 ·
2
Replies
36
Views
10K
  • · Replies 28 ·
Replies
28
Views
12K
  • · Replies 7 ·
Replies
7
Views
3K