Лекция 10. Полнота резолютивного вывода (1161903), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

å. ëèòåðû L11 η1 è L21 η2 óíèôèöèðóåìû.Çíà÷èò, îíè èìåþò ÍÎÓ λ, ò. å.λ ∈ ÍÎÓ(L11 η1 , L21 η2 ), ρ = λµ.Ïîýòîìó äèçúþíêòû-ñêëåéêè D1η1 = Db1η1 ∨ L11η1 èb2 η2 ∨ ¬L21 η2 èìåþò ðåçîëüâåíòó D0 = (Db1 η1 ∨ Db2 η2 )λ,D2 η 2 = Dè ïðè ýòîìb0 ∨ Db0 = Db1 η1 ρ ∨ Db2 η2 ρ = (Db1 η1 ∨ Db2 η2 )λµ = D0 µ.D00 = D12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåb2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2@@η2b1 ∨ L11 ∨ · · · ∨ L1kD1@η1@@ @R@R@@@R@R@b1 η1 ∨ L11 η1 = D1 η1b2 η2 ∨ ¬L21 η2 = D2 η2DDXXXXXλ ρρX9z Xb1 η1 ∨ Db2 η2 )λ(D??000bbD1 ∨ L0 = D1 η1 ρD2 ∨ ¬L00 = D2 η2 ρ@µ@@@@?Rb0 ∨ Db0D12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÒàêèì îáðàçîì, èç äèçúþíêòîâ D1 è D2 ðåçîëþòèâíî âûâîäèìäèçúþíêò D0, îñíîâíûì ïðèìåðîì êîòîðîãî ÿâëÿíòñÿ D00 .×òî è òðåáîâàëîñü äîêàçàòü â ëåììå î ïîäúåìå.Çàâåðøåíèå äîêàçàòåëüñòâà òåîðåìû ïîëíîòû.Ìû ïîêàçàëè, ÷òî1.

Ïðîòèâîðå÷èâàÿ ñèñòåìà äèçúþíêòîâ S èìååò êîíå÷íóþïðîòèâîðå÷èâóþ ñèñòåìó S 0 îñíîâíûõ ïðèìåðîâ (òåîðåìàÝðáðàíà ).2. Èç ïðîòèâîðå÷èâîé ñèñòåìû îñíîâíûõ ïðèìåðîâäèçúþíêòîâ S 0 ìîæíî ðåçîëþòèâíî âûâåñòè ïóñòîéäèçúþíêò (ëåììà îá îñíîâíûõ ïðèìåðàõ ).3. Åñëè ðåçîëþòèâíî âûâîäèì èç ñèñòåìû îñíîâíûõïðèìåðîâ äèçúþíêòîâ S 0, òî ðåçîëþòèâíî âûâîäèì èçèñõîäíîé ñèñòåìû äèçúþíêòîâ S (ëåììà î ïîäúåìå ). ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÌåòîä ðåçîëþöèéI êîððåêòåí,I ïîëîí,I àëãîðèòìèçóåì.Íî êàê ïîëüçîâàòüñÿ èì äëÿ ðåøåíèÿïðàêòè÷åñêèõ çàäà÷?ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÂîò ïîäõîäÿùàÿ ëîãè÷åñêàÿ çàäà÷àÈçâåñòíî, ÷òîI Äàøà ëþáèò Ñàøó,I à Ñàøà ëþáèò ïèâî,I à Ïàøà ëþáèò ïèâî è âñåõ òåõ, êòîëþáèò òî, ÷òî ëþáèò Ïàøà.Âîïðîñ: êòî ëþáèò Äàøó?ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.Âíà÷àëå ñôîðìóëèðóåì çàäà÷ó íà ÿçûêå ëîãèêè ïðåäèêàòîâ.Ñôîðìèðóåì àëôàâèò, ñîñòîÿùèé èç:I Êîíñòàíòû Äàøà ,I Êîíñòàíòû Ñàøà ,I Êîíñòàíòû Ïàøà ,I Êîíñòàíòû ïèâî ,I Ïðåäèêàòíîãî ñèìâîëà L(2) : ¾L(x, y ) x ëþáèò y ¿.ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.Äàëåå çàïèøåì óñëîâèÿ çàäà÷è íà ÿçûêå ëîãèêè ïðåäèêàòîâ.I Äàøà ëþáèò Ñàøó:ϕ1 : L(Äàøà, Ñàøà),I à Ñàøà ëþáèò ïèâî:ϕ2 : L(Ñàøà, ïèâî),I à Ïàøà ëþáèò ïèâî è âñåõ òåõ, êòî ëþáèò òî, ÷òî ëþáèòÏàøà: ϕ3 & ϕ4,ϕ3 : L(Ïàøà, ïèâî).ϕ4 : ∀x (∃y (L(Ïàøà, y ) & L(x, y )) → L(Ïàøà, x))Êòî ëþáèò Äàøó? :.ϕ0 : ∃z L(z, Äàøà)Ôîðìóëèðîâêà çàäà÷è.Ïðîâåðèòü, âåðíî ëè, ÷òî{ϕ1 , ϕ2 , ϕ3 , ϕ4 } |= ϕ0.ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.1.

Ñâîäèì ïðîáëåìó ëîãè÷åñêîãî ñëåäîâàíèÿ{ϕ1 , ϕ2 , ϕ3 , ϕ4 } |= ϕ0ê ïðîáëåìå îáùåçíà÷èìîñòè|= ϕ1 & ϕ2 & ϕ3 & ϕ4 → ϕ0 .2. Ñâîäèì ïðîáëåìó îáùåçíà÷èìîñòè ê ïðîáëåìåïðîòèâîðå÷èâîñòèψ1 = ¬ (ϕ1 & ϕ2 & ϕ3 & ϕ4 → ϕ0 )ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.3. Ñòðîèì ïðåäâàðåííóþ íîðìàëüíóþ ôîðìó ÏÍÔψ2 = ∀x∀y ∀zL(Ñàøà, ïèâî) &L(Ñàøà, ïèâî) &L(Ïàøà, ïèâî) &(¬L(Ïàøà, y ) ∨ ¬L(x, y ) ∨ L(Ïàøà, x)) &¬L(z, Äàøà) .4. Ñòðîèì ñêîëåìîâñêóþ ñòàíäàðòíóþ ôîðìó îíà ñîâïàäàåòñ ÏÍÔ.ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.5.

Ñòðîèì ñèñòåìó äèçúþíêòîâ SS= {D1 = L(Ñàøà, ïèâî),D2 = L(Ñàøà, ïèâî),D3 = L(Ïàøà, ïèâî),D4 = ¬L(Ïàøà, y ) ∨ ¬L(x, y ) ∨ L(Ïàøà, x),D0 = ¬L(z, Äàøà) }.6. À òåïåðü áóäåì ñòðîèòü ðåçîëþòèâíûé âûâîä.Áóäåì ðóêîâîäñòâîâàòüñÿ òàêîé ñòðàòåãèåé:I Íà÷íåì ñ äèçúþíêòà-çàïðîñà D0 ;I Íà êàæäîì øàãå âûâîäà áóäåì èñïîëüçîâàòü ïîñëåäíþþèç ïîñòðîåííûõ ðåçîëüâåíò (ëèíåéíûé âûâîä ).ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD00 = ¬L(z, Äàøà)ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD00 = ¬L(z, Äàøà)D4 = ¬L(Ïàøà, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Ïàøà, x1 )ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD00 = ¬L(z, Äàøà)D4 = ¬L(Ïàøà, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Ïàøà, x1 )θ1 = {z/Ïàøà, x1 /Äàøà}D10 = ¬L(Ïàøà, y1 ) ∨ ¬L(Äàøà, y1 )ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6.

Ëèíåéíûé ðåçîëþòèâíûé âûâîäD00 = ¬L(z, Äàøà)D4 = ¬L(Ïàøà, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Ïàøà, x1 )θ1 = {z/Äàøà, x1 /Äàøà}D10 = ¬L(Ïàøà, y1 ) ∨ ¬L(Äàøà, y1 )D1 = L(Äàøà, Ñàøà)ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD00 = ¬L(z, Äàøà)D4 = ¬L(Ïàøà, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Ïàøà, x1 )θ1 = {z/Äàøà, x1 /Äàøà}D10 = ¬L(Ïàøà, y1 ) ∨ ¬L(Äàøà, y1 ) D1= L(Äàøà, Ñàøà)θ2 = {y1 /Ñàøà}D20 = ¬L(Ïàøà, Ñàøà)ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD00 = ¬L(z, Äàøà)D4 = ¬L(Ïàøà, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Ïàøà, x1 )θ1 = {z/Äàøà, x1 /Äàøà}D10 = ¬L(Ïàøà, y1 ) ∨ ¬L(Äàøà, y1 )D20 = ¬L(Ïàøà, Ñàøà)D1= L(Äàøà, Ñàøà)θ2 = {y1 /Ñàøà}D4 = ¬L(Ïàøà, y2 ) ∨ ¬L(x2 , y2 ) ∨ L(Ïàøà, x2 )ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD00 = ¬L(z, Äàøà)D4 = ¬L(Ïàøà, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Ïàøà, x1 )θ1 = {z/Äàøà, x1 /Äàøà}D10 = ¬L(Ïàøà, y1 ) ∨ ¬L(Äàøà, y1 )D1= L(Äàøà, Ñàøà)θ2 = {y1 /Ñàøà}D20 = ¬L(Ïàøà, Ñàøà) D4 = ¬L(Ïàøà, y2 ) ∨ ¬L(x2 , y2 ) ∨ L(Ïàøà, x2 )θ3 = {x2 /Ñàøà}D30 = ¬L(Ïàøà, y2 ) ∨ ¬L(Ñàøà, y2 )ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6.

Ëèíåéíûé ðåçîëþòèâíûé âûâîäD00 = ¬L(z, Äàøà)D4 = ¬L(Ïàøà, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Ïàøà, x1 )θ1 = {z/Äàøà, x1 /Äàøà}D10 = ¬L(Ïàøà, y1 ) ∨ ¬L(Äàøà, y1 )D20 = ¬L(Ïàøà, Ñàøà)D1= L(Äàøà, Ñàøà)θ2 = {y1 /Ñàøà}D4 = ¬L(Ïàøà, y2 ) ∨ ¬L(x2 , y2 ) ∨ L(Ïàøà, x2 )θ3 = {x2 /Ñàøà}D30 = ¬L(Ïàøà, y2 ) ∨ ¬L(Ñàøà, y2 )ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6.

Ëèíåéíûé ðåçîëþòèâíûé âûâîäD30 = ¬L(Ïàøà, y2 ) ∨ ¬L(Ñàøà, y2 )ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD30 = ¬L(Ïàøà, y2 ) ∨ ¬L(Ñàøà, y2 )D2 = L(Ñàøà, ïèâî)ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD30 = ¬L(Ïàøà, y2 ) ∨ ¬L(Ñàøà, y2 )D40 = ¬L(Ïàøà, ïèâî)D2= L(Ñàøà, ïèâî)θ4 = {y2 /ïèâî}ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD30 = ¬L(Ïàøà, y2 ) ∨ ¬L(Ñàøà, y2 )D40 = ¬L(Ïàøà, ïèâî)D2= L(Ñàøà, ïèâî)θ4 = {y2 /ïèâî}D3 = L(Ïàøà, ïèâî)ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD30 = ¬L(Ïàøà, y2 ) ∨ ¬L(Ñàøà, y2 )D40 = ¬L(Ïàøà, ïèâî)D50 = D2= L(Ñàøà, ïèâî)θ4 = {y2 /ïèâî}D3= L(Ïàøà, ïèâî)θ2 = εÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.6. Ëèíåéíûé ðåçîëþòèâíûé âûâîäD30 = ¬L(Ïàøà, y2 ) ∨ ¬L(Ñàøà, y2 )D40 = ¬L(Ïàøà, ïèâî)D2= L(Ñàøà, ïèâî)θ4 = {y2 /ïèâî}D3= L(Ïàøà, ïèâî)θ5 = εD50 = Óñïåøíûé ðåçîëþòèâíûéâûâîä çàâåðøåí!ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.Èòàê, ñèñòåìà äèçúþíêòîâ S ïðîòèâîðå÷èâà.Çíà÷èò,{ϕ1 , ϕ2 , ϕ3 , ϕ4 } |= ϕ0 . ðàìêàõ íàøåé çàäà÷è ýòî îçíà÷àåò, ÷òî âåðíî óòâåðæäåíèå:¾Êòî-òî ëþáèò Äàøó¿.Íî êòî æå ýòî òàèíñòâåííîå ñóùåñòâî, ëþáÿùååÄàøó?ÏÐÈÌÅÍÅÍÈÅ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÐåøåíèå çàäà÷è.×òîáû îòâåòèòü è íà ýòîò âîïðîñ, âîçüìåì âñåïîäñòàíîâêè-óíèôèêàòîðû, êîòîðûå ìû âû÷èñëèëè ïî õîäóâûâîäà, è ïîñìîòðèì, êàêîå äåéñòâèå îíè îêàæóò íà öåëåâóþïåðåìåííóþ z â äèçúþíêòå-çàïðîñåD0 = ¬L(z, Äàøà).,θ1 = {z/Ïàøà, x1 /Äàøà}θ2 = {y1 /Ñàøà}θ3 = {x2 /Ñàøà}θ4 = {y2 /ïèâî}θ5 = εzθ1 θ2 θ3 θ4 θ5 =ÏàøàÈòàê, Ïàøà ëþáèò Äàøó!ÊÎÍÅÖ ËÅÊÖÈÈ 10..

Характеристики

Список файлов лекций