Skolem-normálforma

A Wikipédiából, a szabad lexikonból.

A Skolem-normálforma (SNF) a matematikai logika elsőrendű logika nevű ágában egy elsőrendű nyelv speciális szimbólumokkal, a Skolem-szimbólumokkal bővített változatának olyan formulája, melynek egyetlen valódi részformulája sem kvantált (mert „a kvantorok mind a formula legelején vannak”, azaz prenex állapotban), továbbá ha előfordul a formulában kvantor, akkor az csak univerzális kvantor lehet.

Tehát általánosan a következő alakú formulák SNF alakúak:

\forall x_{1} \forall x_{2} ... \forall x_{n} \left( M \left( x_{1} , x_{2} , ... , x_{n} \right) \right) ,

ahol M(...), a SNF magja, már kvantormentes formula (lehet nyílt is).

Bebizonyítható, hogy tetszőleges formulához létezik olyan vele egy bizonyos értelemben ekvivalens formula, amely Skolem-normálforma alakú. Ennek előállítására, azaz a formula skolemizálására algoritmusok is adhatóak. Ez tehát - ha prenex formulából indulunk ki, amit a továbbiakban feltételezni fogunk - azt jelenti, hogy „kiküszöböljük a formulából az egzisztenciális kvantorokat” („egy bizonyos értelemben” ekvivalens azért, mert a Skolemizált formula tkp. nem formulája az adott nyelvnek, és így az ekvivalencia definíciója is módosításra szorul).

Tartalomjegyzék

[szerkesztés] Skolemizálás

  1. Először is prenex alakba hozzuk a formulát (ezzel ama cikkben foglalkoztunk) ;
  2. Bevezetjük a Skolem-konstansokat;
  3. Bevezetjük a Skolem-függvényeket;
  4. (Ha tetszik vagy szükséges, akkor a magot KNF, DNF, Zsegalkin- vagy egyéb normálforma alakba is írhatjuk, így kapjuk a Skolem-konjunktív [SKNF], stb. normálformát).

[szerkesztés] A Skolem-konstansok

Legyen

F = Q_{1}x_{1}Q_{2}x_{2}...Q_{n}x_{n} \left( M \left( x_{1} , x_{2} , ... , x_{n} \right) \right)

prenex formula (tehát az M mag kvantormentes).

Ha Q_{1} = Q_{2} = ... = Q_{j} = \exist ( ahol j \le n ), azaz az első néhány kvantor egzisztenciális, akkor F akkor és csak akkor elégíthető ki, ha van olyan interpretáció, melyre a formula igaz, és ekkor (az egzisztenciális kvantor definíciója szerint) az interpretáció U univerzumában kell lennie olyan c1,c2,...,cj elemeknek, hogy ha valamely változókiértékelés során az x1,x2,...,xj változóknak rendre a c1,c2,...,cj , a formula igaz lesz. Ezeket az elemeket Skolem-konstansoknak nevezzük.

A (prenex) formula skolemizálásának első lépése, hogy a nyelvet kibővítjük olyan szimbólumokkal (Skolem-konstansszimbólumok), melyek a fent leírt Skolem-konstansoknak felelnek meg.

Ezután elvégezzük az F formulán az \left( x_{1} , x_{2} , ... , x_{j} || c_{1} , c_{2} , ... , c_{j} \right) termhelyettesítést. Ezzel az első néhány (ha j=n, akkor az összes) egzisztenciális kvantort kiküszöböltük (elimináltuk) a formulából. Ha nem maradt egzisztenciális kvantor a formulában, akkor készen vagyunk, ha meg maradt (de a feltételek miatt Q_{j+1} = \forall, tehát a konstansokkal skolemizált formula már nem egzisztenciális kvantorral „kezdődik”); akkor bevezetjük az ún. Skolem-függvényeket .

[szerkesztés] A Skolem-függvények

Legyen

G = R_{1}x_{1}R_{2}x_{2}...R_{n}x_{n} \left( M \left( x_{1} , x_{2} , ... , x_{n} \right) \right)

olyan prenex formula (tehát az M mag kvantormentes), mely nem egzisztenciális kvantorral kezdődik, azaz melyre igaz R_{1} \ne \exist (ha egzisztenciális kvantorral kezdődik, akkor Skolem-konstansok fentebb leírt bevezetésével mégis elérhető, hogy ilyen alakú legyen).

Legyen tehát a j-1≤n indexig valamennyi Ri univerzális kvantor, míg j-re Rj egzisztenciális! Ha netán j-1=n lenne, akkor készen vagyunk, hiszen feltételeink szerint minden kvantor univerzális. Ha viszont j-1<n, akkor van az Ri kvantorok között valahol egy egzisztenciális. Tehát formulánk a következő alakú:

G = \forall x_{1} \forall x_{2}... \forall x_{j-1} \exist x_{j} R_{j+1}x_{j+1} ... R_{n}x_{n} \left( M \left( x_{1} , x_{2} , ... , x_{j-1} , x_{j} , x_{j+1} , ... , x_{n} \right) \right)

.

Ha ez a formula igaz (pontosabban, ha kielégíthető), az az univerzális kvantifikáció definíciója szerint pontosan azt jelenti, hogy minden x_{1} , x_{2} , ... , x_{j-1} \in U^{j-1} univerzum-(j-1)-eshez létezik olyan xj = cS , amelyre a j-edik (egzisztenciális) kvantor hatóköre mint formula igaz.

Minden elem-(j-1)-eshez tartozik ilyen CS(x1, ... , j-1 ) elem, tehát definiálható az f: Uj-1 &mapsto; U, f(x1, ... , j-1) = f(X) = cS(X) függvény. Ezt a formula megfelelő (tehátb a j-edik) kvantorához vagy változóihoz tartozó Skolem-függvénynek nevezzük.

Nyelvünket bővítsük ki olyan f (a nyelvben eddig nem szereplő) (Skolem-)függvényszimbólummal, melyet később a fentebb leírt f Skolem-függvénnyel interpretálunk. A formula prefixumából (tehát a mag előtt álló kvantorsorozatból) pedig helyjuk el ezt a j-edik, egzisztenciális kvantort, és végezzük el a magban az \left( x_{j} || f \left( x_{1}, ... , x_{j-1} \right) \right) behelyettesítést. Ezzel elimináltunk egy egzisztenciális kvantort a formulából.

[szerkesztés] A Skolemizálás befejezése

A fent leírt két eljárást a formulától függően váltakozva használva - a feltételek által adott, mikor melyiket - addig folytatjuk, míg valamennyi egzisztenciális kvantort nem eliminálunk. A Skolemizálási eljárás véges sok lépésből áll, mivel a formulában csak véges sok egzisztenciális kvantor szerepel, és minden lépésben la. egyet kiejtünk.

[szerkesztés] Példa

[szerkesztés] Elsőrendű klóz

Fő szócikk: elsőrendű klóz.

Egy zárt Skolem-normálformulát, melynek magja konjunktív normálforma alakú, nevezünk elsőrendű klóznak.

[szerkesztés] Hivatkozások

[szerkesztés] Lásd még

  • prenex formula
  • elsőrendű klóz

[szerkesztés] Irodalom

  • Papadimitriou, Christos H.: Számítási bonyolultság (Computational complexity). Egyetemi tankönyv. Novadat Bt., 1999. ISBN 963-9056-20-0 .
  • Pásztorné Varga Katalin – Várterész Magda: A matematikai logika alkalmazásszemléletű tárgyalása, Panem, Bp., 2003. ISBN 963-545-364-7


Ezt a szócikket át kellene olvasni, ellenőrizni a szövegét, tartalmát. További részleteket a cikk vitalapján találhatsz.
Más nyelveken