CNF Rewrite Rules

To obtain CNF, we can perform a series of transformations:

$$\begin{array}{rl}F\to G& \Rightarrow \neg F\vee G\\ F⟺G& \Rightarrow (F\to G)\vee (G\to F)\\ \neg (F\vee G)& \Rightarrow \neg F\wedge \neg G\\ \neg (F\wedge G)& \Rightarrow \neg F\vee \neg G\\ \neg \neg F& \Rightarrow F\\ F\vee (G\wedge H)& \Rightarrow (F\vee G)\wedge (F\vee H)\\ (F\wedge G)\vee H& \Rightarrow (F\vee H)\wedge (G\vee H)\end{array}$$