Boolean normal form (first-order logic)
From Learning Logic for Computer Science
Every first-order formula is equivalent to a formula where the only connectives are 'or', 'and', and 'not'.
A first-order formula is in boolean normal form (BNF) if it is built from atomic formulas using the unary connective $\neg$, the binary connectives $\wedge$ and $\vee$, and existential and universal quantifiers.
An inductive proof, which rewrites every other connective in a straightforward fashion using the rewrite rules for them, can be carried out easily.