Prevesti formulu u prenex normalnu formu: ∀x ((C(x) ∧ ∃y(T(y) ∧ L(x, y))) ⇒ ∃y (D(y) ∧ B(x, y)))
1. eliminacija implikacije. Pošto ćemo dobiti operaciju ∨ koja može da kombinuje izraze pod kvantifikatorima, dolazimo u problem sa y u desnom delu, jer imamo dva "različita" y, koji su vezani za dva egzistencijalna kvantifikatora, sa obe strane implikacije. Zato ćemo desni y da preimenujemo u z, pa onda radimo eliminaciju implikacije
∀x ((C(x) ∧ ∃y(T(y) ∧ L(x, y))) ⇒ ∃z (D(z) ∧ B(x, z)))
∀x ( ¬(C(x) ∧ ∃y(T(y) ∧ L(x, y))) ∨ ∃z (D(z) ∧ B(x, z)) )
2. Izvlačenje kvantifikatora po y ispred, tj. ubacivanje C(x) pod kvantifikator ∃y. Ovo smemo da radimo je je x vezano za spoljni kvantifikator.
∀x ( ¬ ∃y (C(x) ∧ T(y) ∧ L(x, y)) ∨ ∃z (D(z) ∧ B(x, z)))
3. Negacija ¬∃x.A = ∀x.¬A
∀x∀y ( ¬(C(x) ∧ T(y) ∧ L(x, y)) ∨ ∃z (D(z) ∧ B(x, z)))
4. Izvlačenje kvantifikatora po z ispred
∀x∀y∃z ( ¬(C(x) ∧ T(y) ∧ L(x, y)) ∨ (D(z) ∧ B(x, z)) )
I proces je završen, svi kvantifikatori su ispred, formula je u prenex normalnoj formi.
Ako pogledamo formulu, u takvom je obliku da bismo mogli da vratimo implikaciju:
∀x∀y∃z ( (C(x) ∧ T(y) ∧ L(x, y)) ⇒ (D(z) ∧ B(x, z))
Još jedan oblik prenex normalne forme je:
∀x∃z∀y (C(x) ∧ T(y) ∧ L(x, y)) ⇒ (D(z) ∧ B(x, z))
Ne smemo tek tako da premeštamo kvantifikatore. Ovo je ovde moguće zato što smo mogli da izvlačenje kvantifikatora izvršimo drugim raspored (prvo za z pa za y).