Skolem-normálforma

 Ez a szócikk vagy szakasz lektorálásra, tartalmi javításokra szorul. A felmerült kifogásokat a szócikk vitalapja részletezi (vagy extrém esetben a szócikk szövegében elhelyezett, kikommentelt szövegrészek). Ha nincs indoklás a vitalapon (vagy szerkesztési módban a szövegközben), bátran távolítsd el a sablont!
Csak akkor tedd a lap tetejére ezt a sablont, ha az egész cikk megszövegezése hibás. Ha nem, az adott szakaszba tedd, így segítve a lektorok munkáját! (2005 júniusából)

A Skolem-normálforma (SNF) az elsőrendű logikában egy elsőrendű nyelv 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:

∀ x 1 ∀ x 2 … ∀ x n ( M ( x 1 , x 2 , … , x n ) ) {\displaystyle \forall x_{1}\forall x_{2}\dots \forall x_{n}\left(M\left(x_{1},x_{2},\dots ,x_{n}\right)\right)} ,

ahol M ( … ) {\displaystyle M(\dots )} , 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 tulajdonképp nem formulája az adott nyelvnek, és így az ekvivalencia definíciója is módosításra szorul).

Skolemizálás

  1. Először is prenex alakba hozzuk a formulát;
  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álformába is írhatjuk, így kapható Skolem-konjunktív [SKNF] stb. normálforma).

A Skolem-konstansok

Legyen

F = Q 1 x 1 Q 2 x 2 … Q n x n ( M ( x 1 , x 2 , … , x n ) ) {\displaystyle F=Q_{1}x_{1}Q_{2}x_{2}\dots Q_{n}x_{n}\left(M\left(x_{1},x_{2},\dots ,x_{n}\right)\right)}

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

Ha Q 1 = Q 2 = ⋯ = Q j = ∃ {\displaystyle Q_{1}=Q_{2}=\dots =Q_{j}=\exists } ( ahol j ≤ n {\displaystyle j\leq 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 c 1 , c 2 , … , c j {\displaystyle c_{1},c_{2},\dots ,c_{j}} elemeknek, hogy ha valamely változókiértékelés során az x 1 , x 2 , … , x j {\displaystyle x_{1},x_{2},\dots ,x_{j}} változóknak rendre a c 1 , c 2 , … , c j {\displaystyle c_{1},c_{2},\dots ,c_{j}} , 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 ( x 1 , x 2 , … , x j | | c 1 , c 2 , … , c j ) {\displaystyle \left(x_{1},x_{2},\dots ,x_{j}||c_{1},c_{2},\dots ,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 = ∀ {\displaystyle 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 .

A Skolem-függvények

Legyen

G = R 1 x 1 R 2 x 2 … R n x n ( M ( x 1 , x 2 , … , x n ) ) {\displaystyle G=R_{1}x_{1}R_{2}x_{2}\dots R_{n}x_{n}\left(M\left(x_{1},x_{2},\dots ,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 ≠ ∃ {\displaystyle R_{1}\neq \exists } (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 = ∀ x 1 ∀ x 2 … ∀ x j − 1 ∃ x j R j + 1 x j + 1 … R n x n ( M ( x 1 , x 2 , … , x j − 1 , x j , x j + 1 , … , x n ) ) {\displaystyle G=\forall x_{1}\forall x_{2}\dots \forall x_{j-1}\exists x_{j}R_{j+1}x_{j+1}\dots R_{n}x_{n}\left(M\left(x_{1},x_{2},\dots ,x_{j-1},x_{j},x_{j+1},\dots ,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 ∈ U j − 1 {\displaystyle x_{1},x_{2},\dots ,x_{j-1}\in U^{j-1}} univerzum-(j-1)-eshez létezik olyan x j = c S {\displaystyle x_{j}=c_{S}} , amelyre a j-edik (egzisztenciális) kvantor hatóköre mint formula igaz.

Minden elem-(j-1)-eshez tartozik ilyen c S ( x 1 , … , x j − 1 ) {\displaystyle c_{S}(x_{1},\dots ,x_{j-1})} elem, tehát definiálható az f : U j − 1 ↦ U , f ( x 1 , … , x j − 1 ) = f ( X ) = c S ( X ) {\displaystyle f:U^{j-1}\mapsto U,f(x_{1},\dots ,x_{j-1})=f(X)=c_{S}(X)} függvény. Ezt a formula megfelelő (tehát 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 tüntessük el ezt a j-edik, egzisztenciális kvantort, és végezzük el a magban az ( x j | | f ( x 1 , … , x j − 1 ) ) {\displaystyle \left(x_{j}||f\left(x_{1},\dots ,x_{j-1}\right)\right)} behelyettesítést. Ezzel elimináltunk egy egzisztenciális kvantort a formulából.

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.

Példa

Elsőrendű klóz

Bővebben: elsőrendű klóz

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

Források

  • 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

Kapcsolódó szócikkek

  • Prenex-formula
Ez a logikával kapcsolatos lap egyelőre csonk (erősen hiányos). Segíts te is, hogy igazi szócikk lehessen belőle!