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.
A
A ∨ ¬A
A ∧ (B ∨ ¬C) ∧ D
The algorithm has two steps:
⇒
) and equivalence (⇔
) by rewriting using the following equivalences:
A ⇒ B
is equivalent to ¬A ∨ B
A ⇔ B
is equivalent to (¬A ∨ B) ∧ (A ∨ ¬B)
¬
) 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
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
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).
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).
Fitting, Melvin. First-Order Logic and Automated Theorem Proving. Springer, 1990.
Harrison, John. Handbook of Practical Logic and Automated Reasoning. Cambridge, 2009.
Copyright © 2014 Barry Watson. All rights reserved.