Conjunctive normal form

A literal L is either an atom p or the negation of an atom ¬p. If a formula is a conjunction of clauses, where each clause D is a disjunction of literals then it is in conjunctive normal form (CNF), shown as C.

L ::= p | ¬p

D ::= L | L ∨ D

C ::= D | D ∧ C.

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where each clause is a disjunction of literals; it can also be described as an AND of ORs. The conjunctive normal form is useful for automated theorem proving.

Examples of conjunctive normal form formulas

• (¬q ∨ p ∨ r) ∧ (¬p ∨ r) ∧ q
• (p ∨ r) ∧ (¬p ∨ r) ∧ (p ∨ ¬r)

Examples of formulas that are not in conjunctive normal form

• (¬(q ∨ p) ∨ r) ∧ (q ∨ r), since q ∨ p is not a literal
• ¬(q ∨ p), since an OR is nested within a NOT
• p∧( q∨( r∧s) ), since an AND is nested within an OR
• ( p∧ q) ∨ r

The conjunctive normal form allows easy checks of validity which otherwise take exponential times in the number of atoms.

Example: Consider the formula in CNF  (¬q ∨ p ∨ r) ∧ (¬p ∨ r) ∧ q. The semantic entailment ⊨ (¬q ∨ p ∨ r) ∧ (¬p ∨ r) ∧ q holds if and only if all three relations  

⊨¬q ∨ p ∨ r

⊨ ¬p ∨ r

⊨ q

hold, by the semantics of ∧.

Given a formula φ in propositional logic, we say that φ is satisfiable if it has a valuation in which it evaluates to T.
Example: the formula p ∨ q → p is satisfiable since it computes T if we assign T top. P ∨ q → p is not valid.

Thus, satisfiability is a weaker concept since every valid formula is by definition also satisfiable but not the vice versa. Let φ be a formula of propositional logic. Then φ is satisfiable if and only if ¬φ is not valid. Assume that φ is satisfiable. By definition, there exists a valuation of φ in which φ evaluates to T; but that also means that ¬φ evaluates to F for that same valuation. Thus, ¬φ cannot be valid.

Constructing the conjunctive normal form(CNF)

There is a scenario in which computing an equivalent formula in Conjunctive normal form is really easy; namely, when someone else has already done the work of writing down a full truth table for φ. For example, the truth table of (p → ¬q) → (q ∨ ¬p)

For each line where (p → ¬q) → (q ∨ ¬p) computes F, we now construct a disjunction of literals. We have only one conjunct since there is only one such line. That conjunct is now obtained by a disjunction of literals, where we include literals ¬p and q. Note that the literals are just the syntactic opposites of the truth values in that line: here p is T and q is F. The resulting formula in CNF is thus ¬p ∨ q which is readily seen to be in CNF and to be equivalent to (p → ¬q) → (q ∨ ¬p). Thus, φ and the constructed formula CNF have the same truth table.

Consider another example, φ is given by the truth table:

Note that this table is just a specification of φ; it does not tell us what φ looks like syntactically, but it does tell us how it ought to ‘behave.’ Since this truth table has four entries that compute F, we construct four conjuncts ψ_i (1 ≤ i ≤ 4). We read the ψ_i of that table by listing the disjunction of all atoms, where we negate those atoms which are true in those lines:

Ψ₁ def = ¬p ∨ ¬q ∨ r (line 2)

Ψ₂ def = p ∨ ¬q ∨ ¬r (line 5)

Ψ₃ def = p ∨ ¬q ∨ r (line 6)

Ψ₄ def = p ∨ q ∨ ¬r (line 7)

The resulting φ in CNF is, therefore (¬p ∨ ¬q ∨ r) ∧ (p ∨ ¬q ∨ ¬r) ∧ (p ∨ ¬q ∨ r) ∧ (p ∨ q ∨ ¬r).

Disjunctive normal form

A disjunctive normal form (DNF) is a standardization (or normalization) of a logical formula in Boolean logic, which is a disjunction of conjunctive clauses; it can also be described as a sum of products, an OR of ANDs, or (in philosophical logic) a cluster concept.

In other words, if a logical formula is a disjunction of conjunctions with every variable and its negation is present once in each conjunction then it is said to be in disjunctive normal form. All disjunctive normal forms are not unique, as all disjunctive normal forms for the same proposition are mutually equivalent. The disjunctive normal form is widely used in the areas; such as automated theorem proving.

If all the variables involved are represented only once in every clause, a formula is considered as in full disjunctive normal form. Similar to conjunctive normal form, the propositional operators in disjunctive normal form are the same: AND, OR and NOT.

If a statement is a disjunction (sequence of ORs) consisting of one or more disjuncts, each of which is a conjunction (AND) of one or more literals (i.e., statement and negation of statement letters) then it is in disjunctive normal form. The disjunctive normal form is not unique.

Examples of disjunctive normal forms include

• A
• (A ∧ B) ∨ (¬A ∧ C)
• A ∧ B
• A ∨ (B ∧ C)

Where ∨ denotes OR, ∧ denotes AND, and ¬ denotes NOT.

Every statement in logic consisting of a combination of multiple ∧, ∨, and ¬’s can be written in disjunctive normal form.

Constructing the disjunctive normal form(DNF)

• Construct a truth table for the proposition.
• Take the rows of the truth table where the proposition is True to construct minterms
  • If the variable is true, use the propositional variable in the minterm
  • or
  • If a variable is false, use the negation of the variable in the minterm
• Connect the minterms with ∨’s.

Example: How to find the DNF of (p ∨ q) → ¬r

We can set up the DNF from the truth table

(p ∨ q) → ¬r ↔  (p∧q∧¬r) ∨ (p∧¬q∧¬r) ∨ (¬p∧q∧¬r) ∨ (¬p∧¬q∧r) ∨ (¬p∧¬q∧¬r)

Another method or a possible short-cut

Consider the following truth table:

Taking the outputted T’s and following the process given above, the disjunctive normal form will be (p ∧ q) ∨ (¬p ∧ q) ∨ (¬p ∧ ¬q). (Verify!). Notice, though, that in this case there are more outputted trues than falses. The expression can be shortened, and thereby simplified if we take the false outputs instead.

The minister is p ∧ ¬q, but since this matches a false output, it will need to be negated. Hence here the normal form is ¬ (p ∧ ¬q). This will also be considered the disjunctive normal form since there are no other normal forms.

The logic of soundness and completeness