Conjunctive Normal Form

Conjunctive normal form is a structured way of showing propositions to allow them to be resolved more easily. It divides a proposition into disjunctive clauses, joined together by conjunction.

Definition §

Conjunctive Normal Form (CNF)

A proposition, $P$ is in conjunctive normal form iff it can be expressed as:

$$(A_1\vee A_2\vee \dots )\wedge (B_1\vee B_2\vee \dots )\wedge \dots$$

• $A_i,B_i$ are literals, they can either be an atom ($P,Q,R\dots$) or its negation ($\neg$)
• Each pair of brackets surround a disjunctive phrase (literals combined with disjunction$\vee$)
• Hence, a proposition is in CNF if it can be expressed as a conjunction of disjunctive phrases

Clausal Form

CNF can also be expressed as a multiset, known as its clausal form

$$\{\{A_1,A_2,\dots \},\{B_1,B_2,\dots \},\dots \}$$

• Each set represents a disjunctive phrase : $\{A_1,A_2\}$ means $(A_1\vee A_2)$
  • Disjunctive phrases with one literal are singletons : $\{C\}$ means $C$
  • An empty set inside the multiset evaluates to false: $\{\}=\varnothing$ means $\perp$
• Each element in the set is a literal

Because a literal can only be an atom or its negation, for $n$ atoms, we have a maximum of $2n$ literals. There are $2^k$ possible subsets for a set with $k$ elements. The longest clausal form of $n$ atoms would be a multiset consisting of all its subsets. However, we cannot include an empty subset.

Hence, we have $2^{2n}-1$ such phrases in the longest possible clause.

For example:

• One atom ($p$): The longest CF we can create is $\{\{p\},\{\neg p\},\{p,\neg p\}\}$ which has $2^{2\times 1}-1=3$ phrases.
• Two atoms ($p$ and $q$): Has $2^{\{2\times 2\}}-1=15$ phrases

Converting to CNF §

To convert to CNF, we first need to convert to Negation Normal Form (NNF):

1. First convert to NNF:

2. Use distributivity:

It also helps to remove duplicates, tautologies and subsumptions#todo

Theorems §

T1: Every proposition has an logically equivalent CNF

T2: Every unsatisfiable of conjunctives clauses has a refutation

Let $P_{\Sigma }$ be a set of conjunctive clauses.

$$\text{If }{P}_{\Sigma }\models \perp \text{ then }{P}_{\Sigma }{⊢}_R\perp$$

$$P_{\Sigma }\models \perp ⟹P_{\Sigma }{⊢}_R\perp$$

• $P_{\Sigma }\models \perp$ : $P_{\Sigma }$ is unsatisfiable
• $P{⊢}_R\perp$ : $P$ has a refutation
• $⟹$ : Meta-implication (not material implication!)

Examples §

#todo