Normal form for proposition logic

First let's recall some of the symbols used in propositional logic (prior knowledge is asumed).

table 1.

name	symbol	use
atoms	p,q,etc	p
not	$\neg$	$\neg p$
and	$\wedge$	$p \wedge q$
or	$\vee$	$p \vee q$

Using these elements a whole range of expressions can be formed. Most of which are hard to read, and even harder to understand. The (disjunctive) normal form helps to create some order in this chaos. Moreover every expression can be rewritten to this normal form.

The disjunctive normal form has the form of

$$\psi = \alpha \vee \beta_1 \vee \beta_2 \vee .. \vee \beta_n$$

where $\alpha$ is a disjunction of atomic formulas and where $\beta_i$ are conjunctions of atomic formulas. To rewrite any given expression to this form several rules will be needed (table 2).
Note: in this paper the distinction between equivalences and rules is that rules are applied only in one direction (form left to right). So you can get a consistent set of rules that will deterministicly solve your problem without getting stuck in infinite loops.

table 2.

name	rule
DeMorgan	$\neg (p \wedge q)$	$\equiv$	$(\neg p) \vee (\neg q)$
DeMorgan	$\neg (p \vee q)$	$\equiv$	$(\neg p) \wedge (\neg q)$
distribution	$p \wedge (q \vee r)$	$\equiv$	$(p \wedge q) \vee (p \wedge r)$
double negative	$\neg(\neg p)$	$\equiv$	$p$

Using these rules successively whenever applicable will result in disjunctive normal form. In this form every disjunct forms an expression that if true makes the whole expression true, independantly from the other disjuncts.
Unfortunately normalization tends to expand the size of an expression considerably unless some redundancy is removed. To simplify the expression another set of rules are needed form propositional logic (table 3).

table 3.

name	rule
	$p \vee p$	$\equiv$	$p$
	$p \wedge p$	$\equiv$	$p$
falsum	$p \wedge (\neg p)$	$\equiv$	$\bot$
verum	$p \vee (\neg p)$	$\equiv$	$\top$
	$\top \vee p$	$\equiv$	$\top$
	$\bot \vee p$	$\equiv$	$p$
	$\top \wedge p$	$\equiv$	$p$
	$\bot \wedge p$	$\equiv$	$\bot$

Keeping in mind the associative and commutative nature of 'and' and 'or' (and in a sense generalizing the rules in table 3 to that respect), successive application of these rules will reduce redundancy to a great extent, while still preserving normal form.