1.2 Normal forms (conjunctive, disjunctive, negation)

Conversion to Conjunctive Normal Form

Definition and Structure of CNF

Conjunctive normal form (CNF) is a standardized format where a propositional formula is written as a conjunction (AND) of clauses, and each clause is a disjunction (OR) of literals. A literal is just a propositional variable or its negation.

Think of it as: everything at the top level is joined by $\land$, and inside each clause, everything is joined by $\lor$.

Example: $(p \lor q) \land (\neg p \lor r) \land (\neg q \lor \neg r)$

Three clauses, each a disjunction of literals, all connected by AND.

Steps to Convert a Formula to CNF

1. Eliminate implications and biconditionals using logical equivalences.

   • $p \rightarrow q$ becomes $\neg p \lor q$
   • $p \leftrightarrow q$ becomes $(p \rightarrow q) \land (q \rightarrow p)$, then eliminate each implication

2. Push negations inward using De Morgan's laws and double negation elimination, until every negation applies directly to a variable.

   • $\neg(p \land q)$ becomes $\neg p \lor \neg q$
   • $\neg(p \lor q)$ becomes $\neg p \land \neg q$
   • $\neg \neg p$ becomes $p$

3. Distribute $\lor$ over $\land$ to get the final CNF structure.

   • $p \lor (q \land r)$ becomes $(p \lor q) \land (p \lor r)$

Note the direction of distribution in step 3: you're distributing disjunction over conjunction, which produces a conjunction at the top level. The example in the original guide had this backwards.

Properties and Applications of CNF

Every propositional formula can be converted into an equivalent formula in CNF. This universality is what makes CNF so useful as a standard representation.

CNF is the dominant format for satisfiability (SAT) solvers. These tools take a CNF formula and determine whether any truth assignment makes it true. Most modern SAT algorithms (like DPLL and CDCL) are designed specifically to operate on CNF. Automated theorem provers also commonly convert formulas to CNF before applying resolution or other inference rules.

Transformation to Disjunctive Normal Form

Definition and Structure of DNF

Disjunctive normal form (DNF) is the dual of CNF. Here the formula is written as a disjunction (OR) of clauses, where each clause is a conjunction (AND) of literals.

Top level: everything joined by $\lor$. Inside each clause: everything joined by $\land$.

Example: $(p \land q) \lor (\neg p \land r) \lor (q \land \neg r)$

Three clauses, each a conjunction of literals, all connected by OR.

Steps to Convert a Formula to DNF

1. Eliminate implications and biconditionals using the same equivalences as for CNF.

   • $p \rightarrow q$ becomes $\neg p \lor q$

2. Push negations inward using De Morgan's laws until negations apply only to variables.

   • $\neg(p \lor q)$ becomes $\neg p \land \neg q$

3. Distribute $\land$ over $\lor$ to get the final DNF structure.

   • $p \land (q \lor r)$ becomes $(p \land q) \lor (p \land r)$

Notice the contrast with CNF: in step 3, you distribute conjunction over disjunction, which produces a disjunction at the top level.

Properties and Applications of DNF

Every propositional formula can be converted into an equivalent formula in DNF.

DNF is particularly useful for reading off satisfying assignments directly. Each clause in a DNF formula describes one way to make the formula true: if you can satisfy all the literals in any single clause, the whole formula is satisfied. This makes checking satisfiability trivial for DNF (just check whether any clause is consistent), though the conversion itself can produce an exponential blowup in formula size.

Conversely, checking validity (tautology) is hard for DNF but easy for CNF. This duality between the two forms is worth keeping in mind.

Properties of Negation Normal Form

Definition and Structure of NNF

Negation normal form (NNF) is a less restrictive normal form. A formula is in NNF when:

• The only connectives used are $\land$, $\lor$, and $\neg$
• Every negation applies directly to a propositional variable (no negated compound subformulas)

Example: $(p \land \neg q) \lor (\neg p \land r)$

NNF doesn't require any particular arrangement of $\land$ and $\lor$ relative to each other. That's what distinguishes it from CNF and DNF.

Steps to Convert a Formula to NNF

1. Eliminate implications and biconditionals.

   • $p \leftrightarrow q$ becomes $(p \land q) \lor (\neg p \land \neg q)$
   • $p \rightarrow q$ becomes $\neg p \lor q$

2. Push negations inward using De Morgan's laws and double negation elimination until every negation sits directly on a variable.

   • $\neg(p \lor (q \land r))$ becomes $\neg p \land (\neg q \lor \neg r)$
   • $\neg \neg p$ becomes $p$

That's it. No distribution step is needed, which is why NNF conversion doesn't cause the same size explosion that CNF or DNF conversion can.

Properties and Applications of NNF

Every propositional formula has an equivalent NNF, and the conversion is always polynomial in size (unlike CNF/DNF, which can blow up exponentially).

NNF serves as a natural intermediate step on the way to CNF or DNF: steps 1 and 2 of all three conversion procedures are identical. Once you have NNF, you only need the appropriate distribution step to reach CNF or DNF.

Some reasoning systems work directly on NNF. It's also useful for analyzing the polarity of variables in a formula: in NNF, you can immediately see whether a variable appears positively, negatively, or both, which matters for certain proof systems and optimization techniques.

Simplification using Normal Forms

Normal forms give you a common language for comparing and manipulating formulas. Once two formulas are in the same normal form, you can compare their clause sets to check equivalence, identify redundant clauses, or apply transformations systematically.

A few concrete ways normal forms help with simplification:

• Equivalence checking: Convert both formulas to CNF (or DNF), then compare clause sets. If they produce the same set of clauses (up to reordering and removal of duplicates), they're equivalent.
• Identifying tautologies and contradictions: In CNF, a formula is a tautology if every clause is a tautology (contains some variable and its negation). In DNF, a formula is unsatisfiable if every clause is contradictory.
• Clause elimination: In CNF, you can drop clauses that are subsumed by (logically weaker than) other clauses. In DNF, the same applies to redundant disjuncts.

These techniques are foundational for automated theorem provers, SAT solvers, and knowledge representation systems, where keeping formulas compact and in a standard format makes reasoning tractable.