Algorithm to Prenex Normal Form

Any first order formula can be converted into Prenex Normal Form by:

1. Eliminate all occurrences of $\to$ and $\leftrightarrow$ from the formula. Use equivalences from propositional logic: $$\begin{array}{rl}\varphi \to \phi & \equiv \neg \varphi \vee \phi \\ \varphi \leftrightarrow \phi & \equiv (\neg \varphi \vee \phi )\wedge (\varphi \vee \neg \phi )\\ \varphi \leftrightarrow \phi & \equiv (\varphi \wedge \phi )\vee (\neg \varphi \wedge \neg \phi )\end{array}$$
2. Move all negations inward, such that negations only appear in front of atoms. Use equivalences: $$\begin{array}{rl}\neg \neg \varphi & \equiv \varphi \\ \neg \exists x\varphi & \equiv \forall x\neg \varphi \\ \neg \forall x\varphi & \equiv \exists x\neg \varphi \end{array}$$
3. Standardise the variables apart where necessary. Renaming variables in a formula such that distinct variables (not in the scope of the same quantifier) have distinct names.
4. The PNF can now be obtained by moving all quantifiers to the front. Use logic equivalences ($x$ not occurring, or already bound, in $\varphi$): $$\begin{array}{rl}\varphi \wedge (\exists x)\phi & \equiv \exists x(\varphi \wedge \phi )\\ \varphi \wedge (\forall x)\phi & \equiv \forall x(\varphi \wedge \phi )\\ \varphi \vee (\exists x)\phi & \equiv \exists x(\varphi \vee \phi )\\ \varphi \vee (\forall x)\phi & \equiv \forall x(\varphi \vee \phi )\end{array}$$ And other equivalences: $$\begin{array}{rl}(Q_{1}x)\varphi \wedge (Q_{2}y)\phi & \equiv (Q_{1}x)(Q_{2}y)(\varphi \wedge \phi )\\ (Q_{1}x)\varphi \vee (Q_{2}y)\phi & \equiv (Q_{1}x)(Q_{2}y)(\varphi \vee \phi )\end{array}$$