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 ℑ (x1, . . . , xn) formula ℳ to`plamning elementlarini x1, . . . , xn 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
Predikatlar algebrasida inkor amali faqat elementar formulalar oldida kelib, kon’yunksiya, diz’yunksiya, kvantor amallaridan boshqa hech qanday amal qatnashmagan formula normal forma ( formula ) deyiladi. 1 - teorema. Predikatlar algebrasining ixtiyoriy formulasi yo normal forma, yo unga teng kuchli normal forma mavjud.Isbot. Haqiqatdan, agar formulada Þ , Û amallari qatnashsa, ularda
Á Þ Â º ù Á Ú Â , Á Û Â º (ù Á Ú Â ) Ù ( Á Ú ù Â ) tengkuchliliklardan foydalanib Þ , Û amallarni ù , Ù , Ú amallari bilan almashtiramiz. Inkor amali faqat elementar formulalargagina tegishli bo‘lishi uchun
ù ( Á Ù Â ) º ù Á Ú ù Â , ù ( Á Ú Â ) º ù Á Ù ù Â ,
ù ( "x R ( x )) º $x ù R ( x ) , ù ( $x R ( x ) º "x ù R ( x )
tengkuchliliklardan foydalanish etarli.
ta’rif. Predikatlar algebrasining normal formasida kvantorlar qatnashmasa yoki hamma kvantorlar barcha amallardan avval kelsa, bunday forma keltirilgan normal forma yoki preniksli normal forma deyiladi.
