4.4. Elsőrendű klózok

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é'':

Equation 4.. 


Hozzuk a formulát változóiban tiszta alakra:

Equation 4.. 


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:

Equation 4.. 


Példa Írjuk át Skolem-normálformába a

Equation 4.. 


prenexformulát. Először írjuk át a formula magját konjunktív normálformába:

Equation 4.. 


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:

Equation 4.. 


Elsőrendű klózok konjunkciójaként felírva a formulát:

Equation 4.. 


A változóiban tiszta elsőrendű klózhalmaz pedig:

Equation 4..