4.3. Skolem-normálforma
Prev Chapter 4. Normálformák Next

4.3. Skolem-normálforma

A

prenexformulában csak univerzális kvantorok vannak. Az ilyen

alakú formulák fontosak lesznek később.

Definíció Univerzális Skolem-formulának nevezzük az olyan prenexformulát, amelynek a prefixumában csak univerzális kvantor szerepel. Ha a Skolem-formula magja konjunktív normálforma, akkor a formulát Skolem-normálformának nevezzük.

Tétel Tetszőleges

formulához konstruálható olyan univerzális Skolem-formula, mely pontosan akkor kielégíthetetlen, ha

kielégíthetetlen.

Prenexformula ,,átírása'' univerzális Skolem-formába:

  1. Új Skolem-szimbólumok bevezetése: A

    Equation 4.. 


    prenexformula prefixumában legyen az első egzisztenciális kvantor a

    -edik kvantor.

    • Ha

      , akkor minden olyan interpretációban és

      értékelés esetén (

      ), amely mellett

      igaz, az interpretáció

      univerzumában van legalább egy

      ( Skolem-konstans ), hogy a

      formula igaz lesz. Ez azt jelenti, hogy ha kibővítjük az elsőrendű nyelvünket egy új

      konstansszimbólummal, akkor az előbbi interpretációt kiegészítve azzal, hogy

      -t egy Skolem-konstanssal interpretáljuk, az új, bővebb nyelv olyan interpretációját kapjuk, melyben

      is igaz.

    • Legyen most

      . Egy

      interpretációban valamely

      értékelés mellett (

      ) a

      Equation 4.. 


      formula pontosan akkor igaz, ha az

      változókat bármilyen – az interpretáció univerzumából vett – elemekkel értékelve mindig van legalább egy elem

      -ban, amellyel pedig az

      változót értékelve a

      formula igaz. Azaz minden

      elem

      -eshez tartozik legalább egy

      , hogy

      Equation 4.. 


      igaz. Legyen

      Equation 4.. 


      egy függvény, amely minden

      -hez egy ilyen

      értéket rendel. Ezt a függvényt Skolem-függvénynek nevezzük. Bővítsük ki az elsőrendű nyelvünket egy új

      aritású

      függvényszimbólummal. Ha most az

      interpretációt úgy egészítjük ki, hogy

      -et egy ilyen Skolem-függvénnyel interpretáljuk, az új, bővebb nyelv olyan interpretációját kapjuk, melyben a

      Equation 4.. 


      formula igaz.

  2. Az egzisztenciális kvantor elhagyása:

    prefixumából elhagyjuk a

    kvantoros előtagot, és a formula magjában elvégezzük az

    , illetve az

    termhelyettesítést. A kapott

    Equation 4.. 


    illetve

    Equation 4.. 


    formula az eredeti formulában szereplő első egzisztenciális kvantort már nem tartalmazza. Ezzel a lépéssel az eredeti formulával a kielégíthetőség szempontjából egyenértékű formulát kaptunk a kibővített nyelvben.

    1. Egyrészt minden olyan interpretációban, amelyben az eredeti formula valamely értékelés mellett igaz volt, az új függvényszimbólumot (konstansszimbólumot) interpretálhatjuk egy Skolem-függvénnyel (Skolem-konstanssal) úgy, hogy az értékelés mellett igaz lesz az átalakított formula is.

    2. Ha pedig az eredeti formula minden interpretációban, minden értékelés mellett hamis volt, azaz kielégíthetetlen, akkor az átalakított formula is az lesz, mivel ekkor nincs Skolem-függvény (konstans) egyetlen interpretáló struktúrában sem.

  3. Az új Skolem-szimbólumok bevezetésének és a kvantoreliminálásnak a lépéseit végrehajtjuk a soron következő egzisztenciális kvantorra, amíg minden egzisztenciális kvantort el nem hagytunk.

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

Equation 4.. 


prenex-konjunktív formulát. A két egzisztenciális kvantor a prefixum első két kvantora, ezért két Skolem-konstansszimbólumot kell bevezetnünk. Jelöljük az

-tól különböző két új konstansszimbólumot

és

-vel.

Equation 4.. 


Prev Up Next
4.2. Prenex alakú formulák Home 4.4. Elsőrendű klózok