Negation Normal Form (NNF)

A formula in Negation Normal Form (NNF) may comprise of conjunctions, disjunctions, or literals. The negation symbol may only be found in literals. Every formula has an equivalent in NNF.

Examples

	A 
	

	A ∨ ¬A
	

	A ∧ (B ∨ ¬C) ∧ D
	

Transformation Algorithm

The algorithm has two 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

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.

nnf_rewrite_connectives(~A0, ~A1) :- 
	!,
	nnf_rewrite_connectives(A0, A1).
nnf_rewrite_connectives(A0 /\ B0, A1 /\ B1) :-
	!,
	nnf_rewrite_connectives(A0, A1),
	nnf_rewrite_connectives(B0, B1).
nnf_rewrite_connectives(A0 \/ B0, A1 \/ B1) :-
	!,
	nnf_rewrite_connectives(A0, A1),
	nnf_rewrite_connectives(B0, B1).
nnf_rewrite_connectives(A0 => B0, ~A1 \/ B1) :-
	!,
	nnf_rewrite_connectives(A0, A1),
	nnf_rewrite_connectives(B0, B1).
nnf_rewrite_connectives(A0 <=> B0, (~A1 \/ B1) /\ (A1 \/ ~B1)) :-
	!,
	nnf_rewrite_connectives(A0, A1),
	nnf_rewrite_connectives(B0, B1).
nnf_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.

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

The procedure nnf_transform/2 is the entry-point.

nnf_transform(A, C) :-
	nnf_rewrite_connectives(A, B),
	nnf_push_negation(B, C).
	

References

Fitting, Melvin. First-Order Logic and Automated Theorem Proving. Springer, 1990.
Harrison, John. Handbook of Practical Logic and Automated Reasoning. Cambridge, 2009.