Question

a) For the following FOL knowledge base, prove Older(Lulu, Fifi) using resolution.
Mother(Lulu, Fifi)
Alive(Lulu)
∀x ∀y.Mother(x,y) ⇒ Parent(x,y)
∀x ∀y.(Parent(x,y) ∧ Alive(x)) ⇒ Older(x,y)

Answer 1

As per the requirement to prove the fact by using resolution we have to follow some steps:

Steps for Resolution:

1. Step 1:Transformation of fact into FOL.  
2. Step 2: Convert FOL proclamations into CNF
3. Step 3: Negate the explanation which needs to demonstrate (verification by contradiction)
4. Step 4: Draw graph for resolution (unification).

For the given problem follow the step one by one:

Step 1 : The given facts are already present in FOL form so there is no need to do it.

Step 2: For convert FOL into CNF we have to remove all the implication (→) and write the statement again

1) Mother(Lulu, Fifi)
2) Alive(Lulu)
3) ∀x ∀y.Mother(x,y) ⇒ Parent(x,y) ( remove the implication)

  ∀x ∀y ¬Mother(x,y) V Parent(x,y)
4) ∀x ∀y.(Parent(x,y) ∧ Alive(x)) ⇒ Older(x,y) (remove the implication)

∀x ∀y. ¬Parent(x,y) ∨ ¬Alive(x) ∨ Older(x,y)

Step 3: Negate the statements

1)  Mother(Lulu, Fifi)

Negate :  ¬Mother(Lulu, Fifi)

2) Alive(Lulu)

Negate : ¬ Alive(Lulu)

3) Older(x,y)

Negate : ¬ Older(x,y)

4) Parent(x,y)

Negate : ¬ Parent(x,y)

Step 4: Draw the graph of resolution:

  

Thank you..................