Definíció Az elsőrendű klóz pedig egy olyan zárt univerzális Skolem-formula, amelynek a magja elemi diszjunkció.
Egy Skolem-normálforma magja konjunktív normálforma. Ha egy zárt
Skolem-normálformára ,,visszafelé'' alkalmazzuk a konjunkcióra vonatkozó kétoldali kvantorkiemelési szabályt, akkor elsőrendű klózok konjunkcióját kapjuk.
legyen ezen klózok halmaza. Világos, hogy
pontosan akkor kielégíthetetlen, ha
kielégíthetetlen.
Példa Az előző példában kapott Skolem-normálformában alkalmazzuk a kvantorkiemelésre vonatkozó ekvivalenciát ,,visszafelé'':
Hozzuk a formulát változóiban tiszta alakra:
Mivel egy elsőrendű klóz minden változója univerzálisan kvantált,
az
elsőrendű klózhalmazokban a klózok prefixumait nem tüntetjük
fel.
Tehát a fenti elsőrendű klózhalmazt így adjuk meg:
Példa Írjuk át Skolem-normálformába a
prenexformulát.
Először írjuk át a formula magját konjunktív
normálformába:
A Skolem-függvények egyváltozósak, vezessünk be az elsőrendű
nyelvbe
jelölésükre két új függvényszimbólumot:
-et és
-t. A Skolem-normálforma:
Elsőrendű klózok konjunkciójaként felírva a formulát:
A változóiban tiszta elsőrendű klózhalmaz pedig: