Conjunctive Normal Form (CNF)

Conjunctive Normal Form (CNF) is a conjunction of disjunctions of literals. Every formula has an equivalent in CNF.

Examples

	A 
	

	A ∨ ¬A
	

	A ∧ (B ∨ ¬C) ∧ D
	

Transformation Algorithm

There are several different methods for transforming an arbitrary formula into CNF. The following is one of the simplest. This is essentially the method shown in Doets. It has 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 disjunctions (∨) over conjunctions (∧). 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.

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

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

Step 3

Distribute a disjunction over conjunctions where possible. The procedure cnf_distribute/2 performs one such rewriting. The procedure cnf_distribute_loop/2 gives us as many rewritings as possible.

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

cnf_distribute_loop(A, C) :-
	cnf_distribute(A, B),
	!,
	cnf_distribute_loop(B, C).
cnf_distribute_loop(A, A).
       

The procedure cnf_transform/2 is the entry-point.

cnf_transform(A, D) :-
	cnf_rewrite_connectives(A, B),
	cnf_push_negation(B, C),
	cnf_distribute_loop(C, D).
	

References

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