Disjunctive Normal Form (First-Order Logic)

first-order-logic

Definition

Disjunctive Normal Form (First-Order Logic)

A formula is in disjunctive normal form (DNF) if it is a disjunction of conjunctions of literals:

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

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

Conversions

From PNF

From PNF

To bring a formula into DNF:

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

Examples

Example

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