Putting a Formula into Clause Form (p. 285 Tanimoto)

$$(\forall x){P(x) \rightarrow (\exists y){Q(x,y)}} \bigwedge (\forall x){\neg P(x) \rightarrow \neg (\exists y){Q(x,y)}}$$

Step 1: Eliminate implications

$$(\forall x){\neg P(x) \bigvee (\exists y){Q(x,y)}} \bigwedge (\forall x){\neg \neg P(x) \bigwedge \neg (\exists y){Q(x,y)}}$$

Step 2: Reduce the scope of each negation sign. Use DeMorgans if possible Also use:

$$\neg (\forall x)P(x) iff (\exists x) \neg P(x)$$

$$\neg (\exists x)P(x) iff (\forall x) \neg P(x)$$

Also reduce any double negatives.

$$(\forall x){\neg P(x) \bigvee (\exists y){Q(x,y)}} \bigwedge (\forall x){P(x) \bigvee (\forall y){\neg Q(x,y)}}$$

Step 3: Standardize the variables of the formula, giving each quantifier a different name.

$$(\forall x){\neg P(x) \bigvee (\exists y){Q(x,y)}} \bigwedge (\forall z){P(z) \bigvee (\forall w){not Q(z,w)}}$$

Step 4: Eliminate the existential quantifiers using Skolemization

$$(\forall x){\neg P(x) \bigvee Q(x,f(x))} \bigwedge (\forall z){P(z) \bigvee (\forall w){\neg Q(z,w)}}$$

Step 5: Remove the universal quantifiers

$${\neg P(x) \bigvee Q(x, f(x))} \bigwedge {P(z) \bigvee \neg Q(z,w)}$$

Step 6: Put into conjuntive normal form (This function already is)

Distributive Laws may be helpful:

$$P \bigvee (Q \bigwedge R) = (P \bigvee Q) \bigwedge (R \bigvee R)$$

$$P \bigwedge (Q \bigvee R) = (P \bigwedge Q) \bigvee (P \bigwedge R)$$

Step 7: Separate the conjucts into separate clauses:

$$\neg P(x) \bigvee Q(x, f(x))$$

$$P(z) \bigvee \neg Q(z,w)$$