| dbo:abstract
|
- 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: , 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 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). (hu)
- 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: , 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 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). (hu)
|
