Negation Equational Normal Form (NENF)

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

Examples

	A 
	

	A ∨ ¬A
	

	A ∧ (B ⇔ ¬C) ∧ D
	

Transformation Algorithm

The algorithm has two steps:

1. Eliminate the connective for implication (⇒) by rewriting using the following equivalence:
   • A ⇒ B is equivalent to ¬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
   • ¬(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.

nenf_rewrite_connectives(~A0, ~A1) :- 
	!,
	nenf_rewrite_connectives(A0, A1).
nenf_rewrite_connectives(A0 /\ B0, A1 /\ B1) :-
	!,
	nenf_rewrite_connectives(A0, A1),
	nenf_rewrite_connectives(B0, B1).
nenf_rewrite_connectives(A0 \/ B0, A1 \/ B1) :-
	!,
	nenf_rewrite_connectives(A0, A1),
	nenf_rewrite_connectives(B0, B1).
nenf_rewrite_connectives(A0 => B0, ~A1 \/ B1) :-
	!,
	nenf_rewrite_connectives(A0, A1),
	nenf_rewrite_connectives(B0, B1).
nenf_rewrite_connectives(A0 <=> B0, A1 <=> B1) :-
	!,
	nenf_rewrite_connectives(A0, A1),
	nenf_rewrite_connectives(B0, B1).
nenf_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 only equivalences, conjunctions, disjunctions, and negations.

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

The procedure nenf_transform/2 is the entry-point.

nenf_transform(A, C) :-
	nenf_rewrite_connectives(A, B),
	nenf_push_negation(B, C).
	

References

Harrison, John. Handbook of Practical Logic and Automated Reasoning. Cambridge, 2009.