converting FOL to Clause Form

Converting FOL Sentences to Clause Form
Every FOL sentence can be converted to a logically equivalent sentence that is in a "normal form" called clause form
Steps to convert a sentence to clause form:
1.Eliminate all <=> connectives by replacing each instance of the form (P <=> Q) by the equivalent expression ((P => Q) ^ (Q => P))
2Eliminate all => connectives by replacing each instance of the form (P => Q) by (~P v Q)
3Reduce the scope of each negation symbol to a single predicate by applying equivalences such as converting ~~P to P; ~(P v Q) to ~P ^ ~Q; ~(P ^ Q) to ~P v ~Q; ~(Ax)P to (Ex)~P, and ~(Ex)P to (Ax)~P
4.Standardize variables: rename all variables so that each quantifier has its own unique variable name. For example, convert (Ax)P(x) to (Ay)P(y) if there is another place where variable x is already used.
5Eliminate existential quantification by introducing Skolem functions. For example, convert (Ex)P(x) to P(c) where c is a brand new constant symbol that is not used in any other sentence. c is called a Skolem constant. More generally, if the existential quantifier is within the scope of a universal quantified variable, then introduce a Skolem function that depend on the universally quantified variable. For example, (Ax)(Ey)P(x,y) is converted to (Ax)P(x, f(x)). f is called a Skolem function, and must be a brand new function name that does not occur in any other sentence in the entire KB.
Example: (Ax)(Ey)loves(x,y) is converted to (Ax)loves(x,f(x)) where in this case f(x) specifies the person that x loves. (If we knew that everyone loved their mother, then f could stand for the mother-of function.
Remove universal quantification symbols by first moving them all to the left end and making the scope of each the entire sentence, and then just dropping the "prefix" part. For example, convert (Ax)P(x) to P(x).
Distribute "and" over "or" to get a conjunction of disjunctions called conjunctive normal form. Convert (P ^ Q) v R to (P v R) ^ (Q v R), and convert (P v Q) v R to (P v Q v R).
Split each conjunct into a separate clause, which is just a disjunction ("or") of negated and un-negated predicates, called literals.
Standardize variables apart again so that each clause contains variable names that do not occur in any other clause.
Example
Convert the sentence (Ax)(P(x) => ((Ay)(P(y) => P(f(x,y))) ^ ~(Ay)(Q(x,y) => P(y))))
Eliminate <=>Nothing to do here.
Eliminate =>(Ax)(~P(x) v ((Ay)(~P(y) v P(f(x,y))) ^ ~(Ay)(~Q(x,y) v P(y))))
Reduce scope of negation(Ax)(~P(x) v ((Ay)(~P(y) v P(f(x,y))) ^ (Ey)(Q(x,y) ^ ~P(y))))
Standardize variables(Ax)(~P(x) v ((Ay)(~P(y) v P(f(x,y))) ^ (Ez)(Q(x,z) ^ ~P(z))))
Eliminate existential quantification(Ax)(~P(x) v ((Ay)(~P(y) v P(f(x,y))) ^ (Q(x,g(x)) ^ ~P(g(x)))))
Drop universal quantification symbols(~P(x) v ((~P(y) v P(f(x,y))) ^ (Q(x,g(x)) ^ ~P(g(x)))))
Convert to conjunction of disjunctions(~P(x) v ~P(y) v P(f(x,y))) ^ (~P(x) v Q(x,g(x))) ^ (~P(x) v ~P(g(x)))
Create separate clauses
~P(x) v ~P(y) v P(f(x,y))
~P(x) v Q(x,g(x))
~P(x) v ~P(g(x))
Standardize variables
~P(x) v ~P(y) v P(f(x,y))
~P(z) v Q(z,g(z))
~P(w) v ~P(g(w))