Conjunctive Normal Form

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

Definition §

Disjunctive Clause ^definition-disjunctive-clause

A disjunctive clause, $C$, is of the form:

$$C=(P_1\vee P_2\vee \dots )$$

• $P_i$ is a literal, it can either be an atom ($P,Q(x)$) or its negation ($\neg P,\neg Q(x)$)

Conjunctive Normal Form ^definition-cnf

A formula is in conjunctive normal form iff it can be expressed as:

$$C_1\wedge C_2\wedge \dots$$

where $C_i$ is a disjunctive clause. Hence, a formula is in CNF if it can be expressed as a conjunction of disjunctive clauses

Clausal Form ^definition-cf

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 §

Propositional Logic §

In propositional logic, 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

Predicate Logic §

In predicate logic, we still need to obtain a NNF by the same method, but we need to do some additional steps before we can distribute:

1. First, convert to NNF
2. Apply a proper renaming to any shadowed variables
3. Apply a proper renaming such that no two variables in different scopes have the same name.
4. Eliminate any existential quantifiers via Skolemization
5. ‘Hide’ all universally quantifiers (they are still present, just not shown!)
6. Convert to CNF by distributing, same as for propositional:

Theorems §

T1: In propositional logic, every proposition has an logically equivalent CNF

Note that this is not true for predicate logic!

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 §

Propositional Logic §

#todo