Postup převodu sentence do klausálního tvaru

Nejprve vyřešíme, jak pro danou množinu formulí najít množinu klausulí takovou, že množina je splnitelná právě tehdy, když je splnitelná množina . Nepožadujeme, aby množiny a byly tautologicky ekvivalentní, to by totiž obecně nebylo možné. Jedná se tak o obdobu konjunktivní normální formy pro danou formuli ve výrokové logice. Toto nám následně pomůže využít rezoluční metodu pro zjištění, zda daná množina sentencí je splnitelná i zda daná sentence sémanticky vyplývá z dané množiny sentencí. Následující kroky převedou danou sentenci do množiny klausulí .

1. Přejmenujeme proměnné formule tak, aby každý vstup kvantifikátoru vázal jinou proměnnou. (Tj. např. formuli  nahradíme formulí .)
2. Spojky , nahradíme spojkami a na základě známých tautologických rovností
   • nahradíme
   • nahradíme
3. Přesuneme spojku „co nejníže v derivačním stromu formule, tj. až před atomické formule. Použijeme k tomu vztahy
   • nahradíme
   •  nahradíme
   • nahradíme
   •  nahradíme
   • nahradíme
4. Přesuneme spojku „co nejníže v derivačním stromu formule pomocí vztahů
   • nahradíme
   • nahradíme
   • nahradíme

Přitom dáváme přednost první rovnosti. Teprve v případě, že první rovnost nelze aplikovat, používáme další dvě rovnosti. Uvědomte si, že druhá rovnost je opravdu tautologická ekvivalence pouze proto, že formule α neobsahuje proměnnou (viz krok 1).

5. Použijeme tautologickou ekvivalenci a nahradíme  k distribuci obecného kvantifikátoru. Jestliže nyní formule neobsahuje existenční kvantifikátor, máme formuli , která je konjunkcí klausulí. Tuto formuli tedy nahradíme množinou jejích klausulí.
    
6. Obsahuje-li formule existenční kvantifikátor, nahradíme každou uzavřenou podformuli tvaru  formulí , kde je libovolný nový funkční symbol arity . Je-li , použijeme nový konstantní symbol .

Úloha: Převeďme na klausální tvar následující formuli  (jinými slovy, najděte množinu klausulí , která je splnitelná právě tehdy, když je splnitelná sentence ).

Řešení:

Přejmenujeme proměnnou na v podformuli , dostaneme pak .

Krok 2.

Nahradíme spojku : .

Krok 3.

Přesuneme spojku až před atomické formule:

Krok 4 a 5 není potřeba.

Krok 6.

Protože sentence obsahuje existenční kvantifikátory, provedeme skolemizaci. Postupně odstraňujeme existenční kvantifikátory a to v pořadí, v jakém se objevují v derivačním stromu.
, zavedli jsme nový konstantní symbol a místo proměnné x a dosadili ho za všechny výskyty proměnné .
. Zavedli jsme nové konstantní symboly , ; místo proměnné , místo proměnné . Dostali jsme formuli, která je konjunkcí dvou klausulí, proto