View as: 
Two standard forms for first order predicate logic- Prenex normal form requires all the quantifiers to be at the front, whilst Skolem form further demands that only universal (forall) quantifiers are used . Gives an algorithm for finding prenex form with worked example; consideration of Skolem functions; Skolem normal form algorithm; a consideration of logical equivalence and the merits of these normal forms.
you made a typo in page 1
you say
Then replace all ) subformulae with ((¬A) ^ B).
I think you meant ((¬A) v B)
Thanks for the doc though it is very helpfull
Thanks, you’re right of course; pdf is now fixed (somehow the online version was ok!)