"x: [Roman(x)L know(x, Marcus)]® [hate(x ,Caesar) V ("y:$z: hate(y, z) ® think crazy(x ,y))]

1.     Convert the following to clausal form.

"x: [Roman(x)L know(x, Marcus)]® [hate(x ,Caesar) V ("y:$z: hate(y, z) ® think crazy(x ,y))]

Answer: "All Romans who know Marcus either hate Caesar or think that anyone who hates anyone is crazy."

There are 9 simple steps to convert from Predicate logic to clause form.

We will use the following example :
" All Romans who know Marcus either hate Caesar or think that anyone who hates anyone is crazy."

The well formed formula for this statement is :
"x [ Roman(x) and know(x,Marcus)] ® [hate(x,Caesar) Ú ("y($z hate(y,z)) ® thinkcrazy(x,y))]
Lets see each of the covnersion steps in detail :

Well formed formula [ wff] : "x [ Roman(x) and know(x,Marcus)] ® [hate(x,Caesar) Ú ("y($z hate(y,z)) ® think crazy(x,y))]
1. Eliminate ®

We will eliminate implication [ ®] by substituting it with its equivalent.
for e.g. a ® b  =  ~a v b .
Here 'a' and 'b' can be any predicate logic expression.

For the above statement we get :
"x ~[Roman(x) Ù know(x,Marcus)] Ú [hate(x,Caesar) Ú("y~($z hate(y,z)) Ú thinkcrazy(x,y))]
2. Reduce the scope of ~
To reduce the scope we can use 3 rules :
~(~p) = p           
DeMorgans Laws :    ~(aÚb) = ~aÙ~b
                                    ~(aÙb) = ~aÚ~b
Applying this reduction on our example yields :
"x[~Roman(x)Ú~know(x,Marcus)]Ú[hate(x,Caesar)Ú("y"z ~hate(y,z)Úthinkcrazy(x,y))]
3.Change variable names such that, each quantifier has a unique name.
We do this in preparation for the next step. As variables are just dummy names, changing a variable name doesnot affect the truth value of the wff.
Suppose we have
"xP(x) Ú "xQ(x) will be converted to  "x(P(x) Ú "yQ(y) 
4.Move all the quantifiers to the left of the formula without changing their relative order.
As we already have unique names for each quantifier in the previous step, this will not cause a problem.
Performing this on our example we get :
"x"y"z [ ~Roman(x) Ú ~know(x,Marcus)] Ú [ hate(x,Caesar)Ú(~hate(y,z)Úthinkcrazy(x,y))]
5. Eliminate existential quantifiers [ $ ]
We can eliminate the existential quantifier by simply replacing the variable with a reference to a function that produces the desired value.
for eg.
$y President(y) can be transformed into the formula President(S1)
If the existential quantifiers occur within the scope of a universal wuantifier, then the value that satisfies the predicate may depend on the values of the unviersally quantified variables.
For eg..   "x$y fatherof(y,x) will be converted to  "x fatherof( S2(x),x )
6. Drop the Prefix
As we have eliminated all existential quantifiers, all the variables present in the wff are unversally quantified, hence for simplicity we can just drop the prefix, and assume that every variable is universally quantified.
We have form our example :
[ ~Roman(x) Ú ~know(x,Marcus)] Ú [ hate(x,Caesar)Ú(~hate(y,z)Úthinkcrazy(x,y))]
7. Convert into conjunction of disjuncts
As we have no ANDs we will just have to use the associative property to get rid of the brackets.
Incase of ANDs we will need to use the distributive property.
We have :
 ~Roman(x) Ú ~know(x,Marcus) Ú  hate(x,Caesar) Ú ~hate(y,z) Ú thinkcrazy(x,y)
8. Separate each conjunct into a new clause.
As we did not have ANDs in out example, this step is avoided for our example and the final output of the conversion is :

 ~Roman(x) Ú ~know(x,Marcus) Ú  hate(x,Caesar) Ú ~hate(y,z) Ú thinkcrazy(x,y)