Various normal forms of Boolean expressions
Negation normal form of a Boolean expression:
no negation above boolean connectives, quantifiers or relational operators;
no boolean connectives except
Prenex normal form of a Boolean expression: all quantifiers are pushed to the outside and any two quantifiers of the same kind in a row are glued together. Requires expression to be in the negation normal form.