Consider the following axioms:

All people who are graduating are happy.

All happy people smile.

Someone is graduating.

Explain the following:-

1) Represent these axioms in first order predicate logic.

2) Convert each formula to clause form.

3) Prove that ‘’Is someone smiling?’’ using resolution technique. Draw the resolution tree.

1. Represent these axioms in first order predicate logic.

   Object Constant: x = people

   Predicates: G(x) = People Graduating, H(x) = Happy People, S(x) = Smiling People

   FOPL: $\forall x G(x) \forall H(x) \\ \forall x H(x) \forall S(x) \\ \exists x G(x) OR \forall x G(f(x)) ≈ G(y)$

2. Convert each formula to clause form.

   Rules(axioms) : $\forall x G(x) \forall H(x) ; CNF: ¬G(x) v H(x)$

   $\forall x H(x) \forall S(x) ; CNF: ¬H(x) v S(x) \\ Fact: \forall x G(x) Skolemized as G(y) \\ Clause \ \ Forms: \exists x ¬Graduating(x) v Happy(x) \\ \forall x ¬Happy(x) v Smiling(x) \\ \exists x Graduating(x)$

3. Prove that ‘’is someone smiling?’’ using resolution technique. Draw the resolution tree.

   Goal : ¬$\exists$ x Smiling(x) (Negating the Conclusion)

   = $\forall$ x ¬ Smiling(x) //Reduce scope of negation

   Resolution : Standardize variables apart

   $\forall$ x ¬Graduating(x) v Happy(x)

   $\forall$ y ¬Happy(y) v Smiling(y)

   $\exists$ z Graduating(z) : Graduating(someone) // Eliminate $\exists$

   $\forall$ w ¬ Smiling(w)

   Drop all $\forall$

   ¬Graduating(x) v Happy(x)

   ¬Happy(y) v Smiling(y)

   Graduating(someone)

   ¬ Smiling(w)

   Resolution Tree:

Hence proved Someone is smiling!