Conjunctive Normal Form

A propositional formula is in Conjunctive Normal Form (DNF), if it is a Conjunction of Disjunctions of literals, i.e. if it is of the form

⋀_{i = 1}^{n} (⋁_{j = 1}^{m_{i}} ℓ_{i, j})

Where $n, m_{1}, . . ., m_{n} \in N_{> 0}$ and $ℓ_{i, j}$ is a literal
( for every $i \in {1, . . ., n}, j \in {1, . . ., m_{i}}$ )

The sub-formulas $⋁_{j = 1}^{m_{i}} ℓ_{i, j}$ ( for $i \in {1, . . ., n}$ ) are called Disjunctive Clauses.