First-Order Logic: Examples 1-5 Solutions

From Lecture Slides "7. First-Order logic.pdf" (Pages 16-22)

Example 1: Deceivers and Cheaters

1. Anyone who deceives others is considered a cheater

2. Whether intentionally or unintentionally, if anyone ever agree with someone to deceive others, you will be considered a cheater.

3. Because of being timid, there may be people who, in certain circumstances, agree with others to deceive.

Hence, it can be inferred that not everyone who is considered a cheater is not timid.

Step 1: Declaring predicates

Step 2: Knowledge representation

**Premise 1:** Anyone who deceives others is considered a cheater

$$deceiver(x) \rightarrow cheater(x)$$

**Premise 2:** If anyone ever agrees with someone to deceive others, you will be considered a cheater

$$agree(x,y) \land cheater(y) \rightarrow cheater(x)$$

**Premise 3:** Because of being timid, there may be people who agree with others to deceive

$$\exists x (timid(x) \land \exists y(agree(x,y) \land deceiver(y)))$$

$$\neg(\forall x (cheater(x) \rightarrow \neg timid(x)))$$

Which is equivalent to:

$$\exists x (cheater(x) \land timid(x))$$

Step 3: Convert to CNF

**Premise 1:** $deceiver(x) \rightarrow cheater(x)$

$$\neg deceiver(x) \lor cheater(x)$$

**Premise 2:** $agree(x,y) \land cheater(y) \rightarrow cheater(x)$

$$\neg agree(x,y) \lor \neg cheater(y) \lor cheater(x)$$

**Premise 3:** Skolemize $\exists x (timid(x) \land \exists y(agree(x,y) \land deceiver(y)))$

- Let A be a constant for the timid person

- Let B be a constant for the person A agrees with

$$timid(A) \land agree(A,B) \land deceiver(B)$$

Split into clauses:

**Negated Conclusion:** $\exists x (cheater(x) \land timid(x))$

$$\neg \exists x (cheater(x) \land timid(x)) = \forall x (\neg cheater(x) \lor \neg timid(x))$$

CNF form:

$$\neg cheater(x) \lor \neg timid(x)$$

Step 4: Resolution Refutation

**Step 1:** Resolve $C_1$ and $C_5$

- Unify $deceiver(x)$ with $deceiver(B)$: $\sigma = \{x/B\}$

- Resolve with $C_5$: $cheater(B)$

**Step 2:** Resolve $C_4$ and $C_2$ (with $cheater(B)$)

- Unify $agree(A,B)$ with $agree(x,y)$ and use $cheater(y)$

- With substitution $\{x/A, y/B\}$: $\neg agree(A,B) \lor \neg cheater(B) \lor cheater(A)$

- Resolve with $C_4$: $\neg cheater(B) \lor cheater(A)$

- Resolve with $C_7$: $cheater(A)$

**Step 3:** Resolve $C_3$ and $C_6$ (with $cheater(A)$)

- Resolve with $C_8$: $\neg timid(A)$

**Step 4:** Resolve $C_3$ and $C_9$

- Resolve: $\square$ (empty clause - CONTRADICTION!)

Step 5: Conclusion

Since we derived the empty clause, the negation of the conclusion is false, meaning the original conclusion is **TRUE**.

$$\exists x (cheater(x) \land timid(x))$$

There exists a person who is both a cheater and timid.

Example 2: Hung Likes Peanuts

1. Hung likes all kinds of food.

2. Apples are food

3. Chicken is food

4. Anything that people eat and don't get harmed is food

5. Phong ate peanuts and still lived.

6. Lan eats whatever Phong eats.

**Prove:** Hung likes peanuts.

Step 1: Declaring predicates and functions

Step 2: Knowledge representation

**Premise 1:** Hung likes all kinds of food

$$\forall x (Food(x) \rightarrow Likes(hung, x))$$

**Premise 2:** Apples are food

$$Food(apples)$$

**Premise 3:** Chicken is food

$$Food(chicken)$$

**Premise 4:** Anything that people eat and don't get harmed is food

$$\forall x \forall y (Ate(y, x) \land \neg Harmed(y) \rightarrow Food(x))$$

**Premise 5:** Phong ate peanuts and still lived (not harmed)

$$Ate(phong, peanuts) \land \neg Harmed(phong)$$

**Premise 6:** Lan eats whatever Phong eats

$$\forall x (Ate(phong, x) \rightarrow Ate(lan, x))$$

**Conclusion:** Hung likes peanuts

$$Likes(hung, peanuts)$$

Step 3: Convert to CNF

**Premise 1:** $\forall x (Food(x) \rightarrow Likes(hung, x))$

$$\neg Food(x) \lor Likes(hung, x)$$

**Premise 2:** $Food(apples)$

$$Food(apples)$$

**Premise 3:** $Food(chicken)$

$$Food(chicken)$$

**Premise 4:** $\forall x \forall y (Ate(y, x) \land \neg Harmed(y) \rightarrow Food(x))$

$$\neg Ate(y, x) \lor Harmed(y) \lor Food(x)$$

**Premise 5:** $Ate(phong, peanuts) \land \neg Harmed(phong)$

**Premise 6:** $\forall x (Ate(phong, x) \rightarrow Ate(lan, x))$

$$\neg Ate(phong, x) \lor Ate(lan, x)$$

**Negated Conclusion:** $\neg Likes(hung, peanuts)$

$$\neg Likes(hung, peanuts)$$

Step 4: Resolution Refutation

**Step 1:** From Premise 5 and Premise 4

- Resolve with $C_5$: $Harmed(phong) \lor Food(peanuts)$

- Resolve with $C_6$: $Food(peanuts)$

**Step 2:** From Premise 1 and $Food(peanuts)$

- Resolve with $C_9$: $Likes(hung, peanuts)$

**Step 3:** Resolve with negated conclusion

- Resolve: $\square$ (empty clause - CONTRADICTION!)

Step 5: Conclusion

The empty clause is derived, proving that **Hung likes peanuts** is TRUE.

$$Likes(hung, peanuts)$$

Example 3: Mrs. Binh's Cat or Dog

1. All dogs bark at night.

2. Anyone who has a cat has no mice in their house.

3. Anyone who has trouble sleeping does not keep any animal that barks at night.

4. Mrs. Binh has either a cat or a dog.

If Mrs. Binh has trouble sleeping, then there are no mice in her house.

Step 1: Declaring predicates

Step 2: Knowledge representation

**Premise 1:** All dogs bark at night

$$\forall x (Dog(x) \rightarrow BarksAtNight(x))$$

**Premise 2:** Anyone who has a cat has no mice in their house

$$\forall x (Has(person, x) \land Cat(x) \rightarrow \neg HasMice(person's house))$$

Mrs. Binh's house:

$$\forall x (Has(mrsBinh, x) \land Cat(x) \rightarrow \neg HasMice(mrsBinhHouse))$$

**Premise 3:** Anyone who has trouble sleeping does not keep any animal that barks at night

$$\forall x (Has(person, x) \land BarksAtNight(x) \rightarrow \neg TroubleSleeping(person))$$

For Mrs. Binh:

$$\forall x (Has(mrsBinh, x) \land BarksAtNight(x) \rightarrow \neg TroubleSleeping(mrsBinh))$$

Or equivalently:

$$\forall x (TroubleSleeping(mrsBinh) \land Has(mrsBinh, x) \land BarksAtNight(x) \rightarrow \bot)$$

**Premise 4:** Mrs. Binh has either a cat or a dog

$$\exists x ((Has(mrsBinh, x) \land Cat(x)) \lor (Has(mrsBinh, x) \land Dog(x)))$$

**Conclusion:** If Mrs. Binh has trouble sleeping, then there are no mice in her house

$$TroubleSleeping(mrsBinh) \rightarrow \neg HasMice(mrsBinhHouse)$$

Step 3: Convert to CNF

**Premise 1:** $\forall x (Dog(x) \rightarrow BarksAtNight(x))$

$$\neg Dog(x) \lor BarksAtNight(x)$$

**Premise 2:** $\forall x (Has(mrsBinh, x) \land Cat(x) \rightarrow \neg HasMice(mrsBinhHouse))$

$$\neg Has(mrsBinh, x) \lor \neg Cat(x) \lor \neg HasMice(mrsBinhHouse)$$

**Premise 3:** $\forall x (TroubleSleeping(mrsBinh) \land Has(mrsBinh, x) \land BarksAtNight(x) \rightarrow \bot)$

$$\neg TroubleSleeping(mrsBinh) \lor \neg Has(mrsBinh, x) \lor \neg BarksAtNight(x)$$

**Premise 4:** Skolemize (assume Mrs. Binh has animal A)

$$(Has(mrsBinh, A) \land Cat(A)) \lor (Has(mrsBinh, A) \land Dog(A))$$

Distribute:

$$(Has(mrsBinh, A) \land (Cat(A) \lor Dog(A)))$$

Clauses:

**Negated Conclusion:** $TroubleSleeping(mrsBinh) \land HasMice(mrsBinhHouse)$

Step 4: Resolution Refutation

**Step 1:** From $C_5$ (Mrs. Binh has either cat or dog)

We need to split into two cases, but resolution handles this automatically.

- Add $C_8$: $Cat(A)$

**Step 2:** Resolve $C_2$ and $C_4$

- With substitution $\{x/A\}$: $\neg Has(mrsBinh, A) \lor \neg Cat(A) \lor \neg HasMice(mrsBinhHouse)$

- Resolve with $C_4$: $\neg Cat(A) \lor \neg HasMice(mrsBinhHouse)$

- Resolve with $C_8$: $\neg HasMice(mrsBinhHouse)$

**Step 3:** Resolve $C_7$ and $C_9$

- Resolve: $\square$ (empty clause - CONTRADICTION!)

Step 5: Conclusion

The empty clause is derived, proving that if Mrs. Binh has trouble sleeping, then she has no mice in her house.

$$TroubleSleeping(mrsBinh) \rightarrow \neg HasMice(mrsBinhHouse)$$

Example 4: John and His Dog

1. John owns a dog.

2. All people who own dogs are animal lovers.

3. Animal lovers do not kill animals.

**Prove:** John does not kill animals.

Step 1: Declaring predicates

Step 2: Knowledge representation

**Premise 1:** John owns a dog

$$\exists x (Dog(x) \land Owns(john, x))$$

Skolemize: Let $dog_1$ be John's dog

$$Dog(dog_1) \land Owns(john, dog_1)$$

**Premise 2:** All people who own dogs are animal lovers

$$\forall x (Owns(person, x) \land Dog(x) \rightarrow AnimalLover(person))$$

**Premise 3:** Animal lovers do not kill animals

$$\forall x \forall y (AnimalLover(x) \land Animal(y) \rightarrow \neg Kills(x, y))$$

**Conclusion:** John does not kill animals

$$\forall y (Animal(y) \rightarrow \neg Kills(john, y))$$

Step 3: Convert to CNF

**Premise 2:** $\forall x (Owns(person, x) \land Dog(x) \rightarrow AnimalLover(person))$

$$\neg Owns(person, x) \lor \neg Dog(x) \lor AnimalLover(person)$$

**Premise 3:** $\forall x \forall y (AnimalLover(x) \land Animal(y) \rightarrow \neg Kills(x, y))$

$$\neg AnimalLover(x) \lor \neg Animal(y) \lor \neg Kills(x, y)$$

**Negated Conclusion:** $\exists y (Animal(y) \land Kills(john, y))$

Skolemize: Let $victim$ be an animal John kills

Step 4: Resolution Refutation

**Step 1:** From Premise 1 and Premise 2 (John is an animal lover)

$\neg Owns(john, dog_1) \lor \neg Dog(dog_1) \lor AnimalLover(john)$

- Resolve with $C_2$: $\neg Dog(dog_1) \lor AnimalLover(john)$

- Resolve with $C_1$: $AnimalLover(john)$

**Step 2:** From Premise 3

$\neg AnimalLover(john) \lor \neg Animal(victim) \lor \neg Kills(john, victim)$

- Resolve with $C_7$: $\neg Animal(victim) \lor \neg Kills(john, victim)$

- Resolve with $C_3$: $\neg Kills(john, victim)$

**Step 3:** Resolve with negated conclusion

- Resolve: $\square$ (empty clause - CONTRADICTION!)

Step 5: Conclusion

The empty clause is derived, proving that John does not kill animals.

$$\forall y (Animal(y) \rightarrow \neg Kills(john, y))$$

Example 5: Thuy's and An's Hair

1. Thuy is a girl.

2. An is a boy.

3. Girls have longer hair than boys.

**Prove:** Thuy's hair is longer than An's hair.

Step 1: Declaring predicates

Step 2: Knowledge representation

**Premise 1:** Thuy is a girl

$$Girl(thuy)$$

**Premise 2:** An is a boy

$$Boy(an)$$

**Premise 3:** Girls have longer hair than boys

$$\forall x \forall y (Girl(x) \land Boy(y) \rightarrow LongerHairThan(x, y))$$

**Conclusion:** Thuy's hair is longer than An's hair

$$LongerHairThan(thuy, an)$$

Step 3: Convert to CNF

**Premise 3:** $\forall x \forall y (Girl(x) \land Boy(y) \rightarrow LongerHairThan(x, y))$

$$\neg Girl(x) \lor \neg Boy(y) \lor LongerHairThan(x , y)$$

$$\neg LongerHairThan(thuy, an)$$

Step 4: Resolution Refutation

**Step 1:** From Premise 3 with Thuy and An

$\neg Girl(thuy) \lor \neg Boy(an) \lor LongerHairThan(thuy, an)$

- Resolve with $C_1$: $\neg Boy(an) \lor LongerHairThan(thuy, an)$

- Resolve with $C_2$: $LongerHairThan(thuy, an)$

**Step 2:** Resolve with negated conclusion

- Resolve: $\square$ (empty clause - CONTRADICTION!)

Step 5: Conclusion

The empty clause is derived, proving that Thuy's hair is longer than An's hair.

$$LongerHairThan(thuy, an)$$

Summary of Resolution Refutation Method

Key Steps:

1. **Translate** natural language to First-Order Logic

2. **Convert to CNF**: Eliminate implications, move negations, Skolemize

3. **Negate** the conclusion to be proven

4. **Apply Resolution**: Unify complementary literals and resolve

5. **Derive empty clause** (□) to prove the conclusion

Important Notes:

*Generated for First-Order Logic Lecture - Week 11*