Simplify
FormulaRewrites to
P <~> Q (P | Q) & (~P | ~Q)
P <=> Q (P => Q) & (Q => P)
P => Q ~P | Q

Move negations in
FormulaRewrites to
~∀X P ∃X ~P
~∃X P ∀X ~P
~(P & Q) (~P | ~Q)
~(P | Q) (~P & ~Q)
~~P P

Move quantifiers out
FormulaRewrites to
∀X P & Q ∀X (P & Q)
∃X P & Q ∃X (P & Q)
Q & ∀X P ∀X (Q & P)
Q & ∃X P ∃X (Q & P)
∀X P | Q ∀X (P | Q)
∃X P | Q ∃X (P | Q)
Q | ∀X P ∀X (Q | P)
Q | ∃XP ∃X (Q | P)

Skolemize
FormulaRewrites to
Initially Set γ = {}
∀X P P
and set γ = γ ∪ {X}
∃X P P[X/x(γ)]
where x is a new Skolem functor.

Distribute disjunctions
FormulaRewrites to
P | (Q & R) (P | Q) & (P | R)
(Q & R) | P (Q | P) & (R | P)

Convert to CNF
FormulaRewrites to
P1 & ... & Pn {P1,...,Pn}