In: Computer Science
Given the following sentences:
Part 1:
a.)
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))
b.)
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)
5. (a) LS(John)
(b) Have(John, b)
(c) Mouse(b)
we proceed to prove the conclusion by resolution using the above clauses. Each result clause
is numbered; the numbers of its parent clauses are shown at the right-hand side.
6. Cat(a) ∨ Howl(a) [1, 4(b)]
7. ¬Have(x, y) ∨ ¬Cat(y) ∨ ¬Have(x, b) [2, 5(c)]
8. ¬Have(John, y) ∨ ¬Cat(y) [7, 5(b)]
9. ¬Have(John, a) ∨ Howl(a) [6, 8]
10. Howl(a) [4(a), 9]
11. ¬LS(x) ∨ ¬Have(x, a) [3, 10]
12. ¬LS(John) [4(a), 11]
13. [5(a), 12]