In boolean logic, a disjunctive normal form (DNF) is a normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or — in philosophical logic — a cluster concept. The disjunctive normal form and its counterpart, the conjunctive normal form, are the most common standardized ways of representing boolean expressions. They are widely used in various applications such as circuit design or automated theorem proving.

A logical formula is considered to be in DNF if it is a disjunction of one or more conjunctions of one or more literals. A DNF formula is in full disjunctive normal form if each of its variables appears exactly once in every conjunction and each conjunction appears at most once (up to the order of variables). As in conjunctive normal form (CNF), the only propositional operators in DNF are and (${\displaystyle \wedge }$), or (${\displaystyle \vee }$), and not (${\displaystyle \neg }$). The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.

The following is a context-free grammar for DNF:

Where Variable is any variable.

For example, all of the following formulas are in DNF:

The formula ${\displaystyle A\lor B}$ is in DNF, but not in full DNF; an equivalent full-DNF version is ${\displaystyle (A\land B)\lor (A\land \lnot B)\lor (\lnot A\land B)}$.

The following formulas are not in DNF:

In classical logic each propositional formula can be converted to DNF ...