Skolemizace
Máme-li formuli tvaru , podmínku na existenci y můžeme chápat jako podmínku na existenci zobrazení (tzv. výběrové funkce), která pro konkrétní hodnoty konstruuje požadované . Místo uvažované klauzule s existenčním kvantifikátorem tak můžeme uvažovat skolemizovanou formuli . Provedeme-li tuto úpravu s každým existenčním kvantifikátorem zevně dovnitř (vždy při tom volíme nový funkční symbol pro skolemizační funkci), zbavíme se všech existenčních kvantifikátorů. Jedná-li se o funkci nulové arity (), použijeme nový konstantní symbol a, který nazýváme skolemizační konstanta.
Touto úpravou jsme neobdrželi logicky ekvivalentní formuli a interpretace funkční proměnné nebyla nijak stanovena. Půjde nám ale opět jen o splnitelnost. Pro důkaz nesplnitelnosti budeme potřebovat ukázat, že všechny instance proměnných vedou ke sporu - o interpretaci funkce se tak nemusíme zajímat, protože nebude vyhovovat žádná.
Úloha: Proveďte skolemizaci formule