Disjunctive Normal Form (DNF)

Disjunctive Normal Form (DNF) is a disjunction of conjunctions of literals. Every formula has an equivalent in DNF.

Examples

	A 
	

	A ∨ ¬A
	

	A ∨ (B ∧ ¬C) ∨ D
	

Transformation Algorithm

There are several different methods for transforming an arbitrary formula into DNF. The following is one of the simplest with three steps:

1. Eliminate the connectives for implication (⇒) and equivalence (⇔) by rewriting using the following equivalences:
   • A ⇒ B is equivalent to ¬A ∨ B
   • A ⇔ B is equivalent to (¬A ∨ B) ∧ (A ∨ ¬B)
2. Push negations (¬) inside subformulas as far as possible, applying De Morgan's law where possible, and eliminate double negations. We also handle the negation of the propositional constants. We do this by rewriting with the following equivalences:
   • ¬(¬A) is equivalent to A
   • ¬(A ∧ B) is equivalent to ¬A ∨ ¬B
   • ¬(A ∨ B) is equivalent to ¬A ∧ ¬B
   • ¬t is equivalent to f
   • ¬f is equivalent to t
3. Distribute conjunctions (∧) over disjunctions (∨). We rewrite all applicable subterms of the formula using one of the following two equivalences:
   • A ∧ (B ∨ C) is equivalent to (A ∧ B) ∨ (A ∧ C)
   • (A ∨ B) ∧ C is equivalent to (A ∧ C) ∨ (B ∧ C)

Implementation

The following code can be found in the examples directory of the Barry's Prolog distribution.

The following Prolog code in this section implements the algorithm given above. First we fix a set of operators which we will need to represent the formulas of propositional logic.

:-op(200, fy, ~).                   % Negation
:-op(0, yfx, (/\)).
:-op(400, xfy, (/\)).               % Conjunction (not ISO associativity which is yfx)
:-op(0, yfx, (\/)).
:-op(500, xfy, (\/)).               % Disjunction (not ISO associativity which is yfx)
:-op(600, xfy, =>).                 % Implication
:-op(700, xfy, <=>).                % Equivalence
         

Step 1

Eliminate all implications and equivalences.

dnf_rewrite_connectives(~A0, ~A1) :- 
	!,
	dnf_rewrite_connectives(A0, A1).
dnf_rewrite_connectives(A0 /\ B0, A1 /\ B1) :-
	!,
	dnf_rewrite_connectives(A0, A1),
	dnf_rewrite_connectives(B0, B1).
dnf_rewrite_connectives(A0 \/ B0, A1 \/ B1) :-
	!,
	dnf_rewrite_connectives(A0, A1),
	dnf_rewrite_connectives(B0, B1).
dnf_rewrite_connectives(A0 => B0, ~A1 \/ B1) :-
	!,
	dnf_rewrite_connectives(A0, A1),
	dnf_rewrite_connectives(B0, B1).
dnf_rewrite_connectives(A0 <=> B0, (~A1 \/ B1) /\ (A1 \/ ~B1)) :-
	!,
	dnf_rewrite_connectives(A0, A1),
	dnf_rewrite_connectives(B0, B1).
dnf_rewrite_connectives(A, A).
       

Step 2

Recursively push negations, apply De Morgan's law where possible, and eliminate all double negations. At this point there are no implications or equivalences, only conjunctions, disjunctions, and negations.

dnf_push_negation(~(~A0), A1) :- 
	!,
	dnf_push_negation(A0, A1).
dnf_push_negation(~(A0 /\ B0), A1 \/ B1) :-
	!,
	dnf_push_negation(~A0, A1),
	dnf_push_negation(~B0, B1).
dnf_push_negation(~(A0 \/ B0), A1 /\ B1) :-
	!,
	dnf_push_negation(~A0, A1),
	dnf_push_negation(~B0, B1).
dnf_push_negation(A0 /\ B0, A1 /\ B1) :-
	!,
	dnf_push_negation(A0, A1),
	dnf_push_negation(B0, B1).
dnf_push_negation(A0 \/ B0, A1 \/ B1) :-
	!,
	dnf_push_negation(A0, A1),
	dnf_push_negation(B0, B1).
dnf_push_negation(~ true, false).
dnf_push_negation(~ false, true).
dnf_push_negation(A, A).
       

Step 3

Distribute a conjunction over disjunctions where possible. The procedure dnf_distribute/2 performs one such rewriting. The procedure dnf_distribute_loop/2 gives us as many rewritings as possible.

dnf_distribute(A /\ (B \/ C), (A /\ B) \/ (A /\ C)) :- !.
dnf_distribute((A \/ B) /\ C, (A /\ C) \/ (B /\ C)) :- !.
dnf_distribute(A0 /\ B, (A1 /\ B)) :-
	dnf_distribute(A0, A1).
dnf_distribute(A /\ B0, (A /\ B1)) :-
	dnf_distribute(B0, B1).
dnf_distribute(A0 \/ B, (A1 \/ B)) :-
	dnf_distribute(A0, A1).
dnf_distribute(A \/ B0, (A \/ B1)) :-
	dnf_distribute(B0, B1).

dnf_distribute_loop(A, C) :-
	dnf_distribute(A, B),
	!,
	dnf_distribute_loop(B, C).
dnf_distribute_loop(A, A).
       

The procedure dnf_transform/2 is the entry-point.

dnf_transform(A, D) :-
	dnf_rewrite_connectives(A, B),
	dnf_push_negation(B, C),
	dnf_distribute_loop(C, D).
	

References

Chang, C-L, Lee, R C-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
Fitting, Melvin. First-Order Logic and Automated Theorem Proving. Springer, 1990.
Harrison, John. Handbook of Practical Logic and Automated Reasoning. Cambridge, 2009.