# Prenex Normal Form (PNF)

A first-order formula is said to be in Prenex Normal Form (PNF) if it has the form `Q0...Qn-1φ` where `Qi` is a either a universal or existential quantifier, and `φ` is a formula that contains no quantifiers. The sequence `Q0...Qn-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:

1. Eliminate the connectives for implication (`⇒`) and equivalence (`⇔`) by rewriting using the following equivalences:
• `φ ⇒ ψ` is equivalent to `¬φ ∨ ψ`
• `φ ⇔ ψ` is equivalent to `(¬φ ∨ ψ) ∧ (φ ∨ ¬ψ)`
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:
• `¬(¬φ)` is equivalent to `φ`
• `¬(φ ∧ ψ)` is equivalent to `¬φ ∨ ¬ψ`
• `¬(φ ∨ ψ)` is equivalent to `¬φ ∧ ¬ψ`
• `¬t` is equivalent to `f`
• `¬f` is equivalent to `t`
3. 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.