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 (FOL)
2. Use resolution to prove the conclusion (FOL)

Answer 1

Answer :

The very first step is to write each of the axiom as well-formed formula in first-order predicate calculus. The clauses which are written for the above axioms are shown below.

Using LS(x) for `light sleeper'.

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))

Now, the next step is to transform each wff into the Prenex Normal Form, skolemize, and rewrite as clauses in conjunctive normal form.

These transformations are shown below.

1).∀ x (HOUND(x) → HOWL(x))

¬ HOUND(x) ∨ HOWL(x)

2).∀ x ∀ y (HAVE (x,y) ∧ CAT (y) &rarr ¬ ∃ z (HAVE(x,z) ∧ MOUSE (z)))

∀ x ∀ y (HAVE (x,y) ∧ CAT (y) &rarr ∀ 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) &rarr ¬ ∃ 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))] (negated conclusion)

¬ [¬ LS (John) ∨ ¬ ∃ z (HAVE (John, z) ∧ MOUSE(z))]

LS(John) ∧ ∃ z (HAVE(John, z) ∧ MOUSE(z)))

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

The set of CNF clauses for this problem is thus as follows:

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. 1. HAVE(John,a)
   2. CAT(a) ∨ HOUND(a)
5. 1. LS(John)
   2. HAVE(John,b)
   3. MOUSE(b)

Now moving on to prove the conclusion by resolution using the above clauses. Each result clause is numbered.

The numbers of its parent clauses are shown to its left.

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

Thank you!!! Good luck. Stay safe :)