Disjunctive Normal Form

A propositional formula is in Disjunctive Normal Form (DNF), if it is a Disjunction of Conjunctions 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 Conjunctive Clauses.