Predicate into clause form

Question

How would one convert this into clause form?

(1) ∀x[Dog(x) ⇒ Animal(x)]

Some hits, or literally anything is appreciated..!

Thanks in regards, O. Dripp

Answer 1

See Resolution in first order logic :

To recast the reasoning using the resolution technique, first the clauses must be converted to conjunctive normal form (CNF). In this form, all quantification becomes implicit: universal quantifiers on variables ($x, y, \ldots$) are simply omitted as understood, while existentially-quantified variables are replaced by Skolem functions.

Thus, $\forall x \ (Px \to Qx)$ will be converted into :

$\lnot Px \lor Qx$.

---

Assuming that we have to use Resolution with :

(1) $∀x[Dog(x) \to Animal(x)]$, (2) $∀y[Animal(y) \to Die(y)]$ and (3) $Dog(Fido)$

we have to convert them into :

$\lnot Dog(x) \lor Animal(x)$

$\lnot Animal(y) \lor Die(y)$

$Dog(Fido)$.