mavzu. Predikatlar algebrasi formulalarining normal formalari ta’rif

teorema. Predikatlar algebrasining ixtiyoriy formulasi yo keltirilgan normal forma yo unga teng kuchli keltirilgan normal forma mavjud.

XX asrning 40 – yillarida algoritm tushunchasiga aniq ta’rif berilganidan so`ng echilish muammosini hal qilish imkoni hosil bo‘ldi. 1936 yilda amerikalik matematik A.CHyorch predikatlar algebrasi uchun echilish muammosi umumiy holda ijobiy hal qilinmasligini isbot qilgan.

Echilish muammosi chekli sohalar uchun ijobiy hal qilinishi ravshan. Ha=iqatdan, agar ℑ (x₁, . . . , x_n) formula ℳ to`plamning elementlarini x<sub>1</sub>, . . . , x<sub>n</sub> o‘zgaruvchi predmetlar o`rniga qo‘yib chiqib, ℑ formulaning qiymatlarini tekshirib chiqamiz. Bu jarayon chekli qadamda yakunlanadi. Kvantor amallarini esa kon’yunksiya, diz’yunksiya amallari bilan almashtirish mumkin.

1 - misol. "x $u ( R ( x, u, z ) Ú Q ( x )) formula

ℳ = { a, b } to`plamda bajariluvchi bo‘lish bo‘lmasligini aniqash uchun avval formula ko‘rinishini asosiy tengkuchliliklar yordamida o‘zgartiramiz :"x $u ( R ( x, u, z ) Ú Q ( x )) º "x ( P ( x, a, z ) Ú Q ( x ) Ú

Ú R ( x, b, z )) º ( P ( a, a, z ) Ú Q ( a ) Ú P ( a, b, z )) Ù

Ú ( P ( b, a, z ) Ú Q ( b ) Ú P ( b, b, z )).
Hosil bo‘lgan formulada z o`rniga a va b qiymatlarni ketma-ket qo‘yib berilgan formulaning bajariluvchi bo‘lish- bo‘lmasligini aniqash mumkin.

3 -