Prenex Normal Form (PNF)

A first-order formula is said to be in Prenex Normal Form (PNF) if it has the form Q₀...Q_n-1φ where Q_i is a either a universal or existential quantifier, and φ is a formula that contains no quantifiers. The sequence Q₀...Q_n-1 is known as the prefix and φ is known as the matrix. Every formula has an equivalent in PNF.

Examples


		∀x.a(x)


		∀x.∀y.foo(x) ∨ ¬foo(y)


		∃x.∀y.∃z. foo(x,y,z)

Transformation Algorithm

There are several different methods for transforming an arbitrary formula into PNF. The following is one of the simplest. This is essentially the method shown in Doets. It has three sets of transformation rules which are to be applied until they can be applied no more:

Eliminate the connectives for implication (⇒) and equivalence (⇔) by rewriting using the following equivalences:
- φ ⇒ ψ is equivalent to ¬φ ∨ ψ
- φ ⇔ ψ is equivalent to (¬φ ∨ ψ) ∧ (φ ∨ ¬ψ)
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:
- ¬(¬φ) is equivalent to φ
- ¬(φ ∧ ψ) is equivalent to ¬φ ∨ ¬ψ
- ¬(φ ∨ ψ) is equivalent to ¬φ ∧ ¬ψ
- ¬t is equivalent to f
- ¬f is equivalent to t
Rewrite the formula using the following equivalences (from left to right) to pull out quantifiers. Here φ[x/y] is the formula φ where each free occurrence of the variable x is replaced by y. In this case y is a fresh variable, i.e., not used elsewhere in the formula.
- ¬∀x.φ becomes ∃x.¬φ
- ¬∃x.φ becomes ∀x.¬φ
- (∀x.φ ∧ ψ) becomes ∀y.(φ[x/y] ∧ ψ)
- (φ ∧ ∀x.ψ) becomes ∀y.(φ ∧ ψ[x/y])
- (∃x.φ ∧ ψ) becomes ∃y.(φ[x/y] ∧ ψ)
- (φ ∧ ∃x.ψ) becomes ∃y.(φ ∧ ψ[x/y])
- (∀x.φ ∨ ψ) becomes ∀y.(φ[x/y] ∨ ψ)
- (φ ∨ ∀x.ψ) becomes ∀y.(φ ∨ ψ[x/y])
- (∃x.φ ∨ ψ) becomes ∃y.(φ[x/y] ∨ ψ)
- (φ ∨ ∃x.ψ) becomes ∃y.(φ ∨ ψ[x/y])

Implementation

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

First we fix a set of operators which we will need to represent the formulas of first-order logic.

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

The predicate pnf_rewrite_connectives(+A, ?B) takes the formula A and rewrites it to B so that an implication Phi => Psi is replaced by ~Phi \/ Psi and an equivalance Phi <=> Psi is replaced by (~Phi \/ Psi) /\ (Phi \/ ~Psi).


	pnf_rewrite_connectives(~A0, ~A1) :- 
	!,
	pnf_rewrite_connectives(A0, A1).
pnf_rewrite_connectives(A0 /\ B0, A1 /\ B1) :-
	!,
	pnf_rewrite_connectives(A0, A1),
	pnf_rewrite_connectives(B0, B1).
pnf_rewrite_connectives(A0 \/ B0, A1 \/ B1) :-
	!,
	pnf_rewrite_connectives(A0, A1),
	pnf_rewrite_connectives(B0, B1).
pnf_rewrite_connectives(A0 => B0, ~A1 \/ B1) :-
	!,
	pnf_rewrite_connectives(A0, A1),
	pnf_rewrite_connectives(B0, B1).
pnf_rewrite_connectives(A0 <=> B0, (~A1 \/ B1) /\ (A1 \/ ~B1)) :-
	!,
	pnf_rewrite_connectives(A0, A1),
	pnf_rewrite_connectives(B0, B1).
pnf_rewrite_connectives(forall(X, F0), forall(X, F1)) :-
	!,
 	pnf_rewrite_connectives(F0, F1).
pnf_rewrite_connectives(exists(X, F0), exists(X, F1)) :-
	!,
 	pnf_rewrite_connectives(F0, F1).
pnf_rewrite_connectives(A, A).

The predicate pnf_push_negation(+A, -B) rewrites the formula A to B using the following equivalences:

~(~A) <=> A
~(A /\ B) <=> ~A \/ ~B (De Morgan)
~(A \/ B) <=> ~A /\ ~B (De Morgan)
~forall(X, F) <=> exists(X, ~F)
~exists(X, F) <=> forall(X, ~F)
~false <=> true
~true <=> false

The negations are pushed down the formula as much as possible.


	pnf_push_negation(~(~A0), A1) :- 
	!,
	pnf_push_negation(A0, A1).
pnf_push_negation(~(A0 /\ B0), A1 \/ B1) :-
	!,
	pnf_push_negation(~A0, A1),
	pnf_push_negation(~B0, B1).
pnf_push_negation(~(A0 \/ B0), A1 /\ B1) :-
	!,
	pnf_push_negation(~A0, A1),
	pnf_push_negation(~B0, B1).
pnf_push_negation(A0 /\ B0, A1 /\ B1) :-
	!,
	pnf_push_negation(A0, A1),
	pnf_push_negation(B0, B1).
pnf_push_negation(A0 \/ B0, A1 \/ B1) :-
	!,
	pnf_push_negation(A0, A1),
	pnf_push_negation(B0, B1).
pnf_push_negation(~ forall(X, F0), exists(X, F1)) :-
	!,
	pnf_push_negation(~F0, F1).
pnf_push_negation(~ exists(X, F0), forall(X, F1)) :-
	!,
	pnf_push_negation(~F0, F1).
pnf_push_negation(~ true, false) :- !. 
pnf_push_negation(~ false, true) :- !.
pnf_push_negation(A, A).

After a call of pnf_rewrite_variable(+F, +V, +W, -Result) Result is the formula F where every free occurrence of the variable V is rewritten to W.


	pnf_rewrite_variable(F, V, W, W) :-
	var(F),
	F == V,
	!.
pnf_rewrite_variable(F, _, _, F) :-
	var(F),
	% F \== V,
	!.
pnf_rewrite_variable(~A0, V, W, ~A1) :-
	!,
	pnf_rewrite_variable(A0, V, W, A1).
pnf_rewrite_variable(A0 /\ B0, V, W, A1 /\ B1) :-
	!,
	pnf_rewrite_variable(A0, V, W, A1),
	pnf_rewrite_variable(B0, V, W, B1).
pnf_rewrite_variable(A0 \/ B0, V, W, A1 \/ B1) :-
	!,
	pnf_rewrite_variable(A0, V, W, A1),
	pnf_rewrite_variable(B0, V, W, B1).
pnf_rewrite_variable(exists(X, F), V, _, exists(X, F)) :-
	X == V,
	!.
pnf_rewrite_variable(exists(X, F0), V, W, exists(X, F1)) :-
	% X \== V,
	!,
	pnf_rewrite_variable(F0, V, W, F1).
pnf_rewrite_variable(forall(X, F), V, _, forall(X, F)) :-
	X == V,
	!.
pnf_rewrite_variable(forall(X, F0), V, W, forall(X, F1)) :-
	% X \== V,
	!,
	pnf_rewrite_variable(F0, V, W, F1).
pnf_rewrite_variable(Predicate0, V, W, Predicate1) :-
	Predicate0 =.. [F|Args0],
	pnf_rewrite_variable_in_args(Args0, V, W, Args1),
	Predicate1 =.. [F|Args1].

After calling pnf_rewrite_variable_in_args(+Args, +V, +W, -RewrittenArgs) every free occurrence of V in the list Args is rewritten to W giving the result RewrittenArgs.


	pnf_rewrite_variable_in_args([], _, _, []) :- !.
pnf_rewrite_variable_in_args([H0|T0], V, W, [H1|T1]) :- 
	pnf_rewrite_variable(H0, V, W, H1),
	pnf_rewrite_variable_in_args(T0, V, W, T1).

In the predicate pnf_pull_quantifier(+Phi, -Psi) the formula Psi is equivalent to the formula Phi but has had a quantifier pulled out one level of the formula structure.


	pnf_pull_quantifier(forall(X, Phi0) /\ Psi, forall(Y, Phi1 /\ Psi)) :-
	!,
	pnf_rewrite_variable(Phi0, X, Y, Phi1).
pnf_pull_quantifier(Phi /\ forall(X, Psi0), forall(Y, Phi /\ Psi1)) :-
	!,
	pnf_rewrite_variable(Psi0, X, Y, Psi1).
pnf_pull_quantifier(forall(X, Phi0) \/ Psi, forall(Y, Phi1 \/ Psi)) :-
	!,
	pnf_rewrite_variable(Phi0, X, Y, Phi1).
pnf_pull_quantifier(Phi \/ forall(X, Psi0), forall(Y, Phi \/ Psi1)) :-
	!,
	pnf_rewrite_variable(Psi0, X, Y, Psi1).
pnf_pull_quantifier(exists(X, Phi0) /\ Psi, exists(Y, Phi1 /\ Psi)) :-
	!,
	pnf_rewrite_variable(Phi0, X, Y, Phi1).
pnf_pull_quantifier(Phi /\ exists(X, Psi0), exists(Y, Phi /\ Psi1)) :-
	!,
	pnf_rewrite_variable(Psi0, X, Y, Psi1).
pnf_pull_quantifier(exists(X, Phi0) \/ Psi, exists(Y, Phi1 \/ Psi)) :-
	!,
	pnf_rewrite_variable(Phi0, X, Y, Phi1).
pnf_pull_quantifier(Phi \/ exists(X, Psi0), exists(Y, Phi \/ Psi1)) :-
	!,
	pnf_rewrite_variable(Psi0, X, Y, Psi1).
pnf_pull_quantifier(forall(X, F1), forall(X, F2)) :-
	!,
	pnf_pull_quantifier(F1, F2).
pnf_pull_quantifier(exists(X, F1), exists(X, F2)) :-
	!,
	pnf_pull_quantifier(F1, F2).
pnf_pull_quantifier(A0 /\ B, A1 /\ B) :-
	pnf_pull_quantifier(A0, A1),
	!.
pnf_pull_quantifier(A /\ B0, A /\ B1) :-
	pnf_pull_quantifier(B0, B1),
	!.
pnf_pull_quantifier(A0 /\ B, A1 /\ B) :-
	pnf_pull_quantifier(A0, A1),
	!.
pnf_pull_quantifier(A /\ B0, A /\ B1) :-
	pnf_pull_quantifier(B0, B1).

The predicate pnf_pull_all_quantifiers(+Formula, -Result) gives use Result which is Formula where all quantifiers have been pulled out.


	pnf_pull_all_quantifiers(F0, F2) :-
	pnf_pull_quantifier(F0, F1),
	!,
	pnf_pull_all_quantifiers(F1, F2).
pnf_pull_all_quantifiers(F, F).

The predicate pnf_transform(+Phi, -Psi) is the entrypoint. here the formula Psi is a prenex normal form of formula Psi.


	pnf_transform(A, D) :-
	pnf_rewrite_connectives(A, B),
	pnf_push_negation(B, C),
	pnf_pull_all_quantifiers(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.