Home

Prenex Normal Form (PNF)

Move all quantifiers to the front of a first-order logic formula

FOL → PNF
Formula Input
Quantifiers: @x. = ∀x   #x. = ∃x    Connectives: ! & | -> <->   Predicates: P(x,y)  Prop vars: any single letter. Quantifier body requires ( ) if compound.
Prenex Algorithm
φ — Input
↓
Step 1
Eliminate → ↔
↓
Step 2
Push ¬ inward
↓
Step 3
Rename variables
↓
Step 4
Pull quantifiers out
↓
PNF Result
Formula
Enter a formula and click Run ▶
Explanation

Enter a formula and click Run ▶ to start,
then step through the algorithm.