Conjunctive Normal Form (First-Order Logic)

first-order-logic

Definition

Conjunctive Normal Form (First-Order Logic)

A formula is in conjunctive normal form (CNF) if it is a conjunction of clauses, where each clause is a disjunction of literals:

$$\underset{i=1}{\overset{n}{\bigwedge }}\underset{j=1}{\overset{m_i}{\bigvee }}{L}_{ij}$$

Each literal $L_{ij}$ is either an atom or a negated atom.

Conversions

From PNF

From PNF To bring a formula into CNF:

1. Compute the prenex normal form.
2. Convert the quantifier-free matrix to CNF.

Examples

Example

$$(P(x)\vee \neg Q(x,y))\wedge (\neg P(x)\vee R(y))\wedge Q(x,y)$$