# Normal Form

Definition. A literal is a proposition symbol or the negation of a proposition symbol.

A formula is in **conjunctive normal form (CNF)** if it is a conjunction of one or more clauses, where a clause is a disjunction of literals or a single literal.

- Ex: $(¬p∨r)∧(q∨r)$

A formula is in **disjunctive normal form (DNF)** if it is a disjunction of one or more clauses, where a clause is a conjunction of literals or a single literal.

- Ex: $(¬p∧r)∨(q∧r)$

### Converting to CNF / DNF

- Remove all $⟹$ and $⟺$ using
`impl`

and`equiv`

laws. - If the formula in question contains any negated compound subformulas, either remove the negation by using the negation law or use DM to push the negation in.
- Once a formula with no negated compound subformulas is found, use the following distributivity laws.
- For CNF:
- $A∨(B∧C)↔(A∨B)∧(A∨C)$
- $(A∧B)∨C↔(A∨C)∧(B∨C)$

- For DNF:
- $A∧(B∨C)↔(A∧B)∨(A∧C)$
- $(A∨B)∧C↔(A∧C)∨(B∧C)$

- For CNF:
- Simplify so there are no repeated literals in a clause and no two clauses with the same set of literals.
**true**,**false**may appear only if they are the entire formula.

Finding CNF