Question:
Purpose: To apply basic logical inference to a non-trivial example.
The questions below will address the following first-order logic knowledge base (KB).
• ∃x Pail(x) ∧ Fetch(Jack, x)
• ∀x (∃y Pail(y) ∧ Fetch(x, y)) ⇒ Fallen(x)
• ∀x Fallen(x) ⇒ (∀y Needed(y) ⇒ ¬Carries(x, y))
• Carries(Jack, Water) ∨ Carries(Jill, Water)
• Needed(Water)
(a) Express the above formulae in conjunctive normal form (CNF).
(b) Give a resolution proof of the query Carries(Jill, Water). Use the CNF from the previous Part.
What to Hand in
• The given KB expressed in CNF.
• A simple resolution proof of Carries(Jill, Water)