Prenexace

Označme pro tuto www-stránku ¿_j jako symbol pro j-tý kvantifikátor (buď ∀ anebo ∃) a ± je buď ∧ anebo ∨.

Pro další zpracování, převádíme formule do prenexové formy, i. e. do formy, v níž jsou všechny kvantifikátory na začátku formule.

¿1x1 ¿2x2 …  ¿kxk P(x1, x2,  … , xk) ± ¿k+1xi  Q(xi) …	kde i ∈ {1, 2, …, k}, musíme při převodu xi do prenexové formy xi nahradit jinou proměnnou, ale takovou, která není u již „zprenexovaných” kvantifikátorů - v našem případě x1, x2…, xk. V tomto našem případě to může být xk+1 nebo y etc. Tato dílčí transformace náš případ převede například do
¿1x1 ¿2x2  … ¿kxk ¿k+1xk+1 P(x1, x2, … xk) ± Q(xk+1)…  ¿1x1 ¿2x2 …  ¿kxk ¿k+1y P(x1, x2…, xk) ± Q(y)…	anebo do

Poznámka:	Neváží-li se kvantifikátory navzájem, můžeme zaměnit jejich pořadí, což se nám při skolemisaci hodí.
	¿1x1 ¿2x2 …  ¿kxk P(x1, x2,  … , xk) ± ¿k+1xi  Q(xi) …, kde i ∈ {1, 2, …, k} můžeme převést do ¿k+1y (¿1x1  (¿2x2 …  ¿kxk P(x1, x2…, xk)  ± Q(y)…) .
	Kdežto u  ¿1x1 ¿2x2 …  ¿kxk (P(x1, x2,  … , xk) ± ¿k+1xi  Q(xi) …) … to udělat nemůžeme. Předsunování ¿ musíme dělat postupně. První levá závorka může být i mezi ¿ vlevo od její zobrazené posice. Zde je uvedena jen jedna možnost z mnohých ...

Skolemisace

Při skolemisaci eliminujeme existenční kvantifikátory (∃). (Obecné kvantifikátory (∀) ponecháváme.) Pro platnost formule s existenčním kvantifikátorem nám stačí, když bude platná pro právě jeden případ. Konstantní symboly, které se před skolemisací nevyskytovaly — (Skolemovy) konstanty e. g.: a, b, c, c₁, c₂, …, c_k , …, c_n, d …

Funkční symboly, které se před skolemisací nevyskytovaly — (Skolemovy) funktory e. g.: f₁(x₁, …), f₂(x₁,  …), …, f_k(x₁, …), …, f_n(x₁, …).

V případech, kdy před ∃ není žádný ∀ nahrazujeme proměnné jím vázané (Skolemovými) konstantami.
V případech, kdy před ∃ je nějaký ∀ nahrazujeme proměnné vázané oním ∃ (Skolemovými) funktory. Vycházíme z faktu, že funkce přiřazuje, právě jediný prvek (funkční hodnotu) pro všechny prvky z definičního oboru - domémy.

Arita funktorů odpovídá počtu ∀, které předcházejí ∃, jímž vázanou proměnnou nahrazujeme:

∃x∃y∃z P(…, z, … , x, … , y, …)  →   P(…, a, … , b, … , c, …)

∀x∃y∃z P(…, z, … , x, … , y, …)  →   ∀x P(…, f₂(x), … , x, … , f₁(x), …)

∀w∀x∃y∃z P(…, z, … , x, … , y, …)  →   ∀w∀x P(…, f₂(w, x), … , x, … , f₁(w, x), …)

∀x∃y∀z((P(x, y) ∨ ¬Q(z) ∧ (¬R(y) ∨ ¬Q(z))))  →   ∀x∀z((P(x, f(x)) ∨ ¬Q(z) ∧ (¬R(f(x)) ∨ ¬Q(z))))

∀x∃y∀z∃w((P(x, y) ∨ ¬Q(z, w))  →   ∀x∀z((P(x, f₁(x)) ∨ ¬Q(z, f₂(x, z)))