Example CNF for FOL

171 Views Asked by At

I don't understand this example: $\forall x [\forall y\ Animal(y)\Rightarrow Loves(x,y)] \Rightarrow [\exists\ y Loves(y,x)] \\$.

After, I must eliminate biconditionals and implications. In the example i have: $\forall x [\neg\forall y\ \neg Animal(y)\lor Loves(x,y)] \lor [\exists\ y Loves(y,x)] \\$.

I don't understand why when i eliminate the outermost implication, I don't have this situation: $\forall x \neg[\forall y\ \neg Animal(y)\lor Loves(x,y)] \lor [\exists\ y Loves(y,x)] \\$

I apply the rule: $\alpha\Rightarrow\beta$ replaced with $\neg\alpha\lor\beta$.