Question

Given the following sentences:

1. All hounds howl at night.
2. Anyone who has any cats will not have any mice.
3. Light sleepers do not have anything which howls at night.
4. John has either a cat or a hound.
5. (Conclusion) If John is a light sleeper, then John does not have any mice.

1. Negate the conclusion
2. Use resolution to prove the conclusion

Answer 1

a) Negate the conclusion " If John is a light sleeper, then John does not have any mice"

First we convert conclusion in well formed formula (wff) :

LS(John) → ¬ ∃ (z) (Have(John,z) ∧ Mouse(z)) (LS means Light Sleeper)

¬ [LS(John) → ¬ ∃ z (Have(John,z) ∧ Mouse(z))] (negate the conclusion)

¬ [¬ LS (John) ∨ ¬ ∃ z (Have (John, z) ∧ Mouse(z))] (using P --> Q =>  ¬P ∨ Q )

LS(John) ∧ ∃ z (Have(John, z) ∧ Mouse(z)))

Hence, LS(John) ∧ Have(John,b) ∧ Mouse(b)

b)  To prove conclusion using Resolution, First we convert sentences into well formed formula (wff) :-

1. ∀ x (Hound(x) → Howl(x))
2. ∀ x ∀ y (Have(x,y) ∧ Cat(y) → ¬ ∃ z (Have(x,z) ∧ Mouse(z)))
3. ∀ x (LS(x) → ¬ ∃ y (Have(x,y) ∧ Howl(y)))
4. ∃ x (Have(John,x) ∧ (Cat(x) ∨ Hound(x)))
5. LS(John) → ¬ ∃ z (Have(John,z) ∧ Mouse(z))

=> Then we convert well formed formula (wff) into conjunctive normal form (CNF):-

1. ∀ x (Hound(x) → Howl(x))

   ¬ Hound(x) ∨ Howl(x)

2. ∀ x: ∀ y: (Have(x,y) ∧ Cat(y) →   ¬ ∃ z (Have(x,z) ∧ Mouse(z)))

   ∀ x: ∀ y: (Have(x,y) ∧ Cat (y) →  ∀ z ¬ (Have(x,z) ∧ Mouse(z)))

   ∀ x: ∀ y ∀ z (¬ (Have(x,y) ∧ Cat(y)) ∨ ¬ (Have(x,z) ∧ Mouse(z)))

   ¬ Have(x,y) ∨ ¬ Cat(y) ∨ ¬ Have(x,z) ∨ ¬ Mouse(z)

3. ∀ x (LS(x) →  ¬ ∃ y (Have(x,y) ∧ Howl(y)))

   ∀ x (LS(x) → ∀ y ¬ (Have(x,y) ∧ Howl(y)))

   ∀ x ∀ y (LS(x) → ¬ Have(x,y) ∨ ¬ Howl(y))

   ∀ x ∀ y (¬ LS(x) ∨ ¬ Have(x,y) ∨ ¬ Howl(y))

   ¬ LS(x) ∨ ¬ Have(x,y) ∨ ¬ Howl(y)

4. ∃ x (Have(John,x) ∧ (Cat(x) ∨ Hound(x)))

   Have(John,a) ∧ (Cat(a) ∨ Hound(a))

5. ¬ [LS(John) → ¬ ∃ z (Have(John,z) ∧ Mouse(z))]

   ¬ [¬ LS (John) ∨ ¬ ∃ z (Have(John, z) ∧ Mouse(z))]

   LS(John) ∧ ∃ z (Have(John, z) ∧ Mouse(z)))

   LS(John) ∧ HAVE(John,b) ∧ Mouse(b)

=> So, we have set of CNF clauses:-

1. ¬ Hound(x) ∨ Howl(x)
2. ¬ Have(x,y) ∨ ¬ Cat(y) ∨ ¬ Have(x,z) ∨ ¬ Mouse(z)
3. ¬ LS(x) ∨ ¬ Have(x,y) ∨ ¬ Howl(y)
4. a) Have(John,a)   b) Cat(a) ∨ Hound(a)

1. a) LS(John) b) Have(John,b) c) Mouse(b)

=> Resolution Proof:-  In this we cancel the negate predicate with normal predicate

using [1.,4.(b):]	6.	CAT(a) ∨ HOWL(a)
using [2,5.(c):]	7.	¬ HAVE(x,y) ∨ ¬ CAT(y) ∨ ¬ HAVE(x,b)
using [7,5.(b):]	8.	¬ HAVE(John,y) ∨ ¬ CAT(y)
using [6,8:]	9.	¬ HAVE(John,a) ∨ HOWL(a)
using [4.(a),9:]	10.	HOWL(a)
using [3,10:]	11.	¬ LS(x) ∨ ¬ HAVE(x,a)
using [4.(a),11:]	12.	¬ LS(John)
using [5.(a),12:]	13.	□ (null)