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
