10.Предикаттар логикасындағы резолюция әдісі.

а) Резолюция әдісінің анықтамасы.

в) Резолюция әдісін қолдану мысалдары.

Резолюция әдісі

Пікірлер логикасының А формуласының тавтология болу-болмауын қалай тексеруге болады? Бул сураққа Дж. Робинсонның резолюция әдісі жауап береді. Бізге берілген А формулаесы ақиқат болуы үшін оның терістеуі —А кайшылык болуы кажетті және жеткілікті екені белгілі.

Резолюция әдісін сипаттау.

Резолюция әдісін колдану үшін алдымен-A формуласын коньюнктивті нормаланған турге (КНФ) келтіріп аламыз. ОндаD1.. ., D2,...,Dm элементар дизъюнкциялары табылып, —А= D1^D2^...^Dm болады. Онда К={D1, D2,..., Dm} дизъюнктер жиыны деп аталады.Резолюция әдici бойынша, егер Di және Dj дизъюнктарында контрарлы литералдар болса, яғни 6ipiндe пәндік әріп, ал екіншісінде сол әріптің тepicтeyi болса (айталык Di = Dj* v Y,Dj= DjV — Y), онда олар үшiнші дизъюнкті - D*i v D*j резольвентасын құрады.Резольвентада Y, -Y литералдары жоқ. Бұл әрекетті былай белгілейміз:

R

Мысалы ушін = Y,= ¬Yболса, онда оның резольвентасында ешқандай символ жоқ. Мұндай резольвенталарды бос резольвента дейді.

Белгілеуі :□

Теорема 4.13 vрезольвентасы^. Дизъюнктерінің логикалық салдары болады. Яғни,,I-v.

Дэлелдеуі. Бізге l- vvқорытуын дәлелдеу ушін, толықтық туралы теореманы пайдаланыпv қорытуын дәлелдейміз. Одан кешн кейін нәтижені алу үшін дедукция теоремасы колданамыз. Карапайым эквиваленттік қ тынастары қолдану арқылы келесі пара-парлықтарды ~~аламыз. Соңғы формуланы бастапқы өрнекке қойсақ^формуласын аламыз. Бул формуланыңң тавтология болатынына оңай көз жеткізуге болады. Толыктық туралы теорема бойынша бұл формула ПЕ-нің теремасы. Демек, жоғарыдағы қорыту^дұрыс. Теорема дәлелденді. Жалпы жағдайда бастапқы формуланың тавтология болатынын дәлелдеу үшін ол формуланыц терістеуін КНФ түрне келтіріп,резольвента алу ережесшін бірнеше кайта қолдану арқылы бос резольвента алуға ұмтыламыз. Яғни қайшылыққа келуге тырысамыз. Бастапқы формула тавтология болса, бұл әдістің нәтижесі міндетті турде қайшылық болуға тиіс. Қайшылық әдеттесимволымен белгіленеді.

Теорема 4.14 (Kepi жорып дәлелдеу принципі). Г формулалар жиыны, ал А формула болсын. Егер Г, ¬A болса, онда Г|-А болады. Дәлелдеуі. Г¬А болса, онда дедукция теоремасынан Г, ¬A. Албоғандықтан, |- Г —> А. Демек, ГА.

Енді резолюция алгроритмінің әр қадамын сипаттап берейік.

Резолюция әдісінің алгоритмі.

А формуласыныц терістеуін А енгіземіз.

А формуласын КНФ туріне келтіреміз.

Оныц дизъюнктерінің жиынын К={ D1, D2,..., Dm} құрамыз.К жиынының парларына талдау жасайьқ: егер және дизъюнктерінің бірінде X, ал екіншісіндеХ болса, онда бұлдизъюнктерге 6ipiгуін құрып, оның резольвентасын табамыз. Яғни жоғарыдағы 6ipiгуден контрарлық литералдарды X және Х-ті аластаймыз.Егер табылған резольвента бос болса, онда 6i3 мақсатымызға жеттік. Яғни алынған қайшыльқ, берілген формуланың тавтология болатындығын керсетеді. Kepi жағдайда, табылған резольвентаны дизъюнктер жиынына қосып, төртінші қадамға көшеміз.

Бул алгоритмді орындағанда келесі жағдай орын алуы мумкін.

Берілген дизъюнктер К={ D1, D2,..., Dm} жиынынан резольвента құрылмайды. Онда берілген формула тавтология болмайды. Кандай да 6ip қадамда, бос резольвента пайда болады. Онда берілген формула тавтология.

Резольвента табу npoцeci тоқтамайды. Бұл жағдайда берілген формуланың ақиқаттығы туралы ештеңе айта алмаймыз.Резолюция әдісі берілген формуланың қандай да 6ip формулалар жиынының салдары болатынын дәлелдеу үшін де қолдануға болады.Айталық , F1, F2, ..., Fm В қорытуын дәлелдеу ушін—>B қорытуын дәлелдеу керек. Ал—>B]vВ. Демек, A =vВ формуласы тавтология болу yшінA =В) формуласы кайшылық болуы керек. Ары қарай резолюция әдісі алгоритмін қолданып, аталган формуланың қайшылық болатынын дәлелдейміз.

1- ші мысал. X, В, (СX—>В)Сқорытуын дәлелдейік.

Шешуі:

Онда А = (X В(СХ—>В)) —>C деп алсақ,

А =[( XВ(СХ—>В)) —>C)] Онда осы

Формуланың тepicтeyiн табамыз.

А =( X В(СХ—>В)) —>C) Ал

СХ—>ВC vX vB және (С)~С болады, онда= XВ(СХ. Демек, дизъюнктер жиыны К = {Х,В,СХ,C} болғандықтан. С Х және С дизъюнктерінің резольвентасы X v болады. Сондықтан, К = {X, В,СХ,X v, С}. Онда В жәнедизъюнктерінің резольвентасы бос резольвента болады. Демек

берілген қорыту дұрыс.

11.Предикаттар есептеуі.

а) Гильберттік аксиомалар нұсқалары.

в)Предикаттар есептеуінің қорыту ережелері.

Предикаттар есептеуі. Аксиомалар нұсқалары мен қорыту ережелері.

Предикаттар логикасының касиомалық негізде құрылған формалды теориясын предикаттар теориясы деп атаймыз. Предикаттар есептеуінің алфавитін, формулаларын предикаттар логикасындағыдай анықтаймыз. Осы формулалар жиынының қандай да бір бөлігі аксиомалар деп жарияланып және оның қорыту епежелері анықталады. Осылар арқылы предикаттар логикасының теоремалары дәлелденеді.

Аксиомалар нұсқалары.

Г1.

Г2.

Г3.

Г4.

Г5.

Г6.

Г7.

Г8.))

Г9.

Г10.

Г11.

Г12.

Жоғарғыда келтірілген нұсқалардан фибпси және тетта формулаларының кездесулерін предикаттар есептеуінің кез келген формуласымен ауыстыру арқылы алынған жаңа формулалар предикаттар есептеуінің аксиомалары деп аталады.

Предикаттар есептеуінде 3 қорыту ережесі бар:

1. Оқылуы:формуласыжәнеформулаларының тікелей салдары болады. Бұл қорыту ережесін MP(modus ponens) ережесі деп атайды.

2. . Оқылуы:формуласыформуласының тікелей салдары болады.

3. . Оқылуы:∃ y формуласыформуласының тікелей салдары болады.

12. Предикаттар есептеуіндегі қорыту.

а) Қорытудың анықтамасы. Қарапайым қасиеттері.

Егер ,...,формулалар тізбегіндегі әрбәр формула аксиома немес өзінің алдындағы формулалардың тікелей салдары болса, оны предикаттар есептеуінің қорытуы (дәлелдеуі) деп айтамыз. Соңғы формуласы φ болатын предикаттар есептеуінің қорытуы табылса, φ формуласын предикаттар есептеуінің теорремасы деп атаймыз. Белгіленуі: ├ φ

Егер ,...,формулаларының әрбіреуі аксиома немесе Г формулалар жиынының элементі немесе өзінің алдындағы формулалардың қорыту ережелерінің бірі бойынша тікелей салдары болса, бұл тізбекті Г жиынындағы қорыту деп айтамыз. Егер соңғы формуласы φ формуласына тең предикаттар есептеуінің Г жиынындағы қорытуы табылса, онда φ формуласын Г жиынында қорытылады немесе Г жиынының салдары деп атаймыз. Белгілеуі Г├φ.

Соңғы анықтамадағы φ формуласы бос жиынның тікелей салдары болса, онда φ формуласы предикатар есептеуінің теоремасы болатыны түсінікті.

Предикаттар есептеуінде үш қорыту ережесі бар.

I. . Оқылуы: ψформуласы φ және φ→ψ формулаларының тікелей салдары болады.Бұл қорыту ережесін МР (modus ponens) ережесі деп атайды.

II. . Оқылуы:формуласыформуласының тікелей салдары болады.

III. . Оқылуыформуласыформуласының тікелей салдары болады.

Ескертулер: 1. Егер формуласы қорытудағы ϴ→ φ(v) немесе φ(v)→ϴ формулаларының бірінің II ережесінің немесе III ереженің бірінің тікелей салдары болса, v айнымлысыформуласының алдындағы ешір формулада бос айнымалы болып кездеспеуі керек.

2. Предикаттар есептеуіндегі қорыту ұғымының қарапайым қасиеттері пікірлер есептеуіндегі қорытудың қарапайым қасиеттерімен толығымен сай келеді. Атап айтқанда әрбір аксиома – теорема, кез келген теорема – кез келген формулалар жиынының салдары және егер формула қандай да бір жиынның салдары болса, ол формула аталған жиынды қамтитын кез келген жиынның салдары болады. Сонымен бірге қорытудың транзитивтілік және финиттілік қасиеттері де орындалады.

в) Теорема ұғымы және оның үлгілері.

Егер соңғы формуласы φ формуласына тең предикаттар есептеуінің Г жиынындағы қорытуы табылса, онда φ формуласын Г жиынында қорытылады немесе Г жиынының салдары деп атаймыз. Егер соңғы формуласы φ болса предикаттар есептеуінің теоремасы деп атаймыз.

Предикаттар есептеуіндегі қорыту ұғымының қарапайым қасиеттері пікірлер есептеуіндегі қорытудың қарапайым қасиеттерімен сай келеді. Атап айтқанда әрбір аксиома – теорема, кез кезген теорема - кез келген формулалар жиынының салдары болады.

Егер Г предикаттар есептеуінің формулалар жиыны, ал φ және ψ предикаттар есептеуінің формулалары болса, онда Г → {φ} ├ ψ <=> Г ├ φ → ψ.

Жеке жағдайы: φ ├ ψ <=> ├ φ → ψ. (Айтылуы: Егер ψ формуласы φ формуласының салдары болса, онда φ → ψ формуласы теорема болады)

Дәлелдеуі: (=>): Егер қорыту бір ғана формуладан тұрса, яғни n=1 болса, онда үш жағдай болуы мүмкін:

1.ψ = φ. Онда ├ φ → φ болғандықтан ├ φ → ψ. Яғни Г ├ φ → ψ.

2. ψ є Г. Онда Г├ ψ. Бұдан ├ ψ → (φ → ψ) аксиомасына және Г├ ψ қорытуына MP ережесін қолдансақ, Г├ φ → ψ болады.

3. ψ – предикаттар есептеуінің аксиомасы болсын. Онда Г├ ψ және ├ ψ → (φ → ψ) қорытуларына МР ережесін қолдану нәтижесінде Г├ φ → ψ болады.

Егер ψ формуласы өзінің алдындағы қандай да бір формуладан III-ші ереже арқылы алынса, бұл жағдай алдыңғы жағдайға ұқсас дәлелденеді.

(<=). Бұл импликацияның дәлелдеуі пікірлер есептеуінде келтірілген дәлелдеуді толығымен қайталайды. Теорема дәлелденді.