Лекции В.А. Захарова (1157993), страница 15

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

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

S 0 ïðîòèâîðå÷èâàÿ ñèñòåìà, âåðíî I 6|= S10 ∪ S20 ∪ S30 .Ò. ê. I |= A0 è S10 = {D : D ∈ S 0, D = Db ∨ A0}, âåðíî I |= S10 .Çíà÷èò, I 6|= S20 ∪ S30 .Âîçìîæíû äâà âàðèàíòà.Âàðèàíò 1. I 6|= S30 . Òîãäà I 6|= S 00, ÷òî è òðåáîâàëîñü.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''$'S01b1 ∨ A0D$S02$'íåò ëèòåð A0, ¬A0b2 ∨ ¬A0D&&%&%&b1 ∨ Db2D&&%%$''S0 $S03S00'$S00 $S03íåò ëèòåð A0, ¬A0&%%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''$'S01trueb1 ∨ A0D$S02$'íåò ëèòåð A0, ¬A0b2 ∨ ¬A0D&&%&%&b1 ∨ Db2D&&%%$''S0 $S03S00'$S00 $S03íåò ëèòåð A0, ¬A0&%%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0DÂàðèàíò 1.S02b2 ∨ ¬A0D$S0 $S03$'íåò ëèòåð A0, ¬A0I 6|= D&&%&%&$''b1 ∨ Db2D&&%%S00'$S00 $S03íåò ëèòåð A0, ¬A0&%%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0DÂàðèàíò 1.S02$S0 $S03$'íåò ëèòåð A0, ¬A0b2 ∨ ¬A0DI 6|= D&&%&%&$''b1 ∨ Db2D&&%%S00$'S00 $S03íåò ëèòåð A0, ¬A0I 6|= D%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Âàðèàíò 2.

I 6|= S20 .Çíà÷èò, ñóùåñòâóåò òàêîé äèçúþíêò Db2 ∨ ¬A0 ∈ S20 , ÷òîb2 ∨ ¬A0 . Ñëåäîâàòåëüíî, I 6|= Db2 (ïî÷åìó? ).I 6|= DÐàññìîòðèì òåïåðü èíòåðïðåòàöèþ I 0, êîòîðàÿ îòëè÷àåòñÿ îò Iòîëüêî òåì, ÷òî I 0 6|= A0.Ò. ê. I 0 6|= S10 ∪ S20 ∪ S30 (âåäü S 0 ïðîòèâîðå÷èâàÿ),b ∨ ¬A0 } è I 0 |= ¬A0 ),I 0 |= S20 (âåäü S20 = {D : D ∈ S 0 , D = D00I |= S3 (à èíà÷å ìû áû èìåëè âàðèàíò 1, âåäü A0 ∈/ S30 ),âåðíî I 0 6|= S10 .Çíà÷èò, ñóùåñòâóåò òàêîé äèçúþíêò Db1 ∨ A0 ∈ S10 , ÷òîb1 ∨ A0 . Ñëåäîâàòåëüíî, I 0 6|= Db1 . À ïîñêîëüêó A0 ∈b1 , à II 0 6|= D/D0îòëè÷àåòñÿ îò I òîëüêî îöåíêîé àòîìà A0, âåðíî I 6|= Db1 .ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0D&&Âàðèàíò 2.S02b2 ∨ ¬A0D%&b1 ∨ Db2D&&true$S03%%$S00$'S00 $S03íåò ëèòåð A0, ¬A0%&$íåò ëèòåð A0, ¬A0%&''$'S0%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0DÂàðèàíò 2.S02b2 ∨ ¬A0D'$true$S0$S03íåò ëèòåð A0, ¬A0b2I 6|= D&&%&%&$''b1 ∨ Db2D&&%%S00$'S00 $S03íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI |= A0''S01true$'b1 ∨ A0DÂàðèàíò 2.S02b2 ∨ ¬A0D'$true$S0$S03íåò ëèòåð A0, ¬A0b2I 6|= D&&%&%&$''S00b1 ∨ Db2D&&%%b2I 6|= D$'S00 $S03íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI0 6|= A0''S01$'b1 ∨ A0DÂàðèàíò 2.S02b2 ∨ ¬A0D'$true$S0$S03íåò ëèòåð A0, ¬A0b2I 6|= D&&%&%&$''S00b1 ∨ Db2D&&%%b2I 6|= D$'S00 $S03íåò ëèòåð A0, ¬A0%&%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI0 6|= A0''S01'$S02b1 ∨ A0Db2 ∨ ¬A0Db1I0 6|= Db2I 6|= D&&%&'$trueíåò ëèòåð A0, ¬A0%%$'S00b1 ∨ Db2Db2I 6|= D$'S00 $S03íåò ëèòåð A0, ¬A0%&$S0 $S03%&'&&Âàðèàíò 2.%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI0 6|= A0''S01'$S02b1 ∨ A0Db2 ∨ ¬A0Db1I0 6|= Db2I 6|= D&&%&trueíåò ëèòåð A0, ¬A0%%$'S00b1 ∨ Db2Db1I0 6|= D'$b2I 6|= D$'S00 $S03íåò ëèòåð A0, ¬A0%&$S0 $S03%&'&&Âàðèàíò 2.%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀI0 6|= A0''S01'$S02b1 ∨ A0Db2 ∨ ¬A0Db1I0 6|= Db2I 6|= D&&%&trueíåò ëèòåð A0, ¬A0%%$S00b1 ∨ Db2Db1 ∨ Db2I 6|= D&&'$$'S00 $S03íåò ëèòåð A0, ¬A0%&$S0 $S03%&''Âàðèàíò 2.%%ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Âàðèàíò 2.Ò.ê.

I 6|= Db1 è I 6|= Db2, âåðíî I 6|= Db1 ∨ Db2.Îñòàåòñÿ çàìåòèòü, ÷òî Db1 ∨ Db2 ýòî ðåçîëüâåíòà äèçúþíêòîâb2 ∨ ¬A0 ∈ S 0 è Db1 ∨ A0 ∈ S 0 , è ïîýòîìó Db1 ∨ Db2 ∈ S 0D210ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Âàðèàíò 2.Ò.ê. I 6|= Db1 è I 6|= Db2, âåðíî I 6|= Db1 ∨ Db2.Îñòàåòñÿ çàìåòèòü, ÷òî Db1 ∨ Db2 ýòî ðåçîëüâåíòà äèçúþíêòîâb2 ∨ ¬A0 ∈ S 0 è Db1 ∨ A0 ∈ S 0 , è ïîýòîìó Db1 ∨ Db2 ∈ S 0D210000Ñëåäîâàòåëüíî, I 6|= S0. Òîãäà I 6|= S , ÷òî è òðåáîâàëîñü.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû.Âàðèàíò 2.Ò.ê. I 6|= Db1 è I 6|= Db2, âåðíî I 6|= Db1 ∨ Db2.Îñòàåòñÿ çàìåòèòü, ÷òî Db1 ∨ Db2 ýòî ðåçîëüâåíòà äèçúþíêòîâb2 ∨ ¬A0 ∈ S 0 è Db1 ∨ A0 ∈ S 0 , è ïîýòîìó Db1 ∨ Db2 ∈ S 0D210000Ñëåäîâàòåëüíî, I 6|= S0.

Òîãäà I 6|= S , ÷òî è òðåáîâàëîñü.Èòàê, â îáîèõ ñëó÷àÿõ I 6|= S 00. Ò. ê. I ïðîèçâîëüíàÿèíòåðïðåòàöèÿ, ïðèõîäèì ê çàêëþ÷åíèþ î òîì, ÷òî ñèñòåìàäèçúþíêòîâ S 00 = S00 ∪ S30I ïðîòèâîðå÷èâàÿ,I ïîëó÷åíà èç S 0 ïðè ïîìîùè ïðàâèëà ðåçîëþöèè,I íå ñîäåðæèò àòîìà A0 .Èíäóêòèâíûé ïåðåõîä çàâåðøåí, è ëåììà äîêàçàíà.ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà î ïîäúåìåÏóñòü D1 è D1 äâà äèçúþíêòà, è ïðè ýòîì VarD ∩ VarD = ∅.Ïóñòü D10 = D1θ è D20 = D2θ äâà îñíîâíûõ ïðèìåðà ýòèõäèçúþíêòîâ D1 è D1.Ïóñòü D00 ðåçîëüâåíòà äèçúþíêòîâ D10 è D20 .Òîãäà èç äèçúþíêòîâ D1 è D2 ðåçîëþòèâíî âûâîäèì äèçúþíêòD0 , îñíîâíûì ïðèìåðîì êîòîðîé ÿâëÿåòñÿ äèçúþíêò D00 .12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà î ïîäúåìåD1D2?D10?D20= D1 θ@@@@R@D00= D2 θÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà î ïîäúåìåD1D2@@@@@RD0?D10?D20= D1 θ@@@@R@?D00= D2 θÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀËåììà î ïîäúåìåD1D2@@@@@RD0?D106?D20= D1 θ@@@@R@?D00= D2 θÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÏóñòü L00, ¬L00 ýòî êîíòðàðíàÿ ïàðà ëèòåð, ïî êîòîðîé áûëàïîñòðîåíà ðåçîëüâåíòà D00 äèçúþíêòîâ D10 è D20 .b 0 ∨ L0 ,D10 = D1000b ∨ ¬L0 ,D2 = D20b0 ∨ Db0 .D00 = D12Ïîñêîëüêó VarD ∩ VarD = ∅, ïîäñòàíîâêó θ ìîæíî ðàçäåëèòüíà äâå ïîëîâèíû θ1, θ2 òàê, ÷òî12θ = θ1 ∪ θ2 , Domθ1 ⊆ VarD1 , Domθ2 ⊆ VarD2 .ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåD1D2??b 0 ∨ L0 = D1 θ1D10b 0 ∨ ¬L0 = D2 θ2D20@@@@R@b0b0 ∨ DD12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÏîñêîëüêó D10 = D1θ1, ëèòåðà L00 ÿâëÿåòñÿ îñíîâíûì ïðèìåðîìíåêîòîðûõ ëèòåð L11, L12, .

. . , L1k , âõîäÿùèõ â ñîñòàâäèçúþíêòà D1, ò.å.L00 = L11 θ = L11 θ1 = · · · = L1k θ1 .Àíàëîãè÷íî, ëèòåðà ¬L00 ÿâëÿåòñÿ îñíîâíûì ïðèìåðîìíåêîòîðûõ ëèòåð ¬L21, ¬L22, . . . , ¬L2k , âõîäÿùèõ â ñîñòàâäèçúþíêòà D2, ò. å.¬L00 = ¬L21 θ2 = ¬L22 θ2 = · · · = ¬L2k θ2 .Çíà÷èò,1122b1 ∨ L11 ∨ L12 ∨ · · · ∨ L1kD1 = D1b2 ∨ ¬L21 ∨ ¬L22 ∨ · · · ∨ ¬L2kD2 = D2ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåb2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2b1 ∨ L11 ∨ · · · ∨ L1kD1θ1@θ2@@ @R@R@@@@@R@b 0 ∨ L0 = D1 θ1D10R@b 0 ∨ ¬L0 = D2 θ2D20@@@@@Rb0 ∨ Db0D12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÒàê êàê L00 = L11θ = L12θ1 = · · · = L1k θ1, ëèòåðûL11 , L12 , . .

. , L1k óíèôèöèðóåìû. Çíà÷èò, îíè èìåþò ÍÎÓ η1 ,ò. å.η1 ∈ ÍÎÓ(L11 , L12 , . . . , L1k ), θ1 = η1 ρ1 .Çíà÷èò D1η1 ñêëåéêà äèçúþíêòà D1 ïî ëèòåðàìL11 , L12 , . . . , L1k , è ïðè ýòîì D10 = D1 θ1 = (D1 η1 )ρ1 îñíîâíîéïðèìåð ñêëåéêè D1η2.Àíàëîãè÷íî, ëèòåðû ¬L21, ¬L22, . . . , ¬L2k èìåþò ÍÎÓ η2.Òîãäà D2η2 ñêëåéêà äèçúþíêòà D2 ïî ëèòåðàì¬L21 , ¬L22 , .

. . , ¬L2k , è ïðè ýòîì D20 = D2 θ2 = (D1 η2 )ρ2 îñíîâíîé ïðèìåð ñêëåéêè D2η2.111122ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåb2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2@@η2b1 ∨ L11 ∨ · · · ∨ L1kD1@η1@@ @R@R@@b1 η1 ∨ L11 η1 = D1 η1Dρ1?@R@??b 0 ∨ L0 = D1 η1 ρ1D10R@b2 η2 ¬ ∨ L21 η2 = D2 η2Dρ2?b 0 ∨ ¬L0 = D2 η2 ρ2D20@@@@@Rb0b0 ∨ DD12ÏÎËÍÎÒÀ ÐÅÇÎËÞÒÈÂÍÎÃÎ ÂÛÂÎÄÀÄîêàçàòåëüñòâî ëåììû î ïîäúåìåÑîãëàñíî íàøåé ïðèâû÷êå ïåðåèìåíîâûâàòü ïåðåìåííûå,äèçúþíêòû-ñêëåéêè D1η1 è D2η2 ñîäåðæàò ðàçíûå íàáîðûïåðåìåííûõ. Ïîýòîìó Domρ ∩ Domρ = ∅, è ñóùåñòâóåòïîäñòàíîâêà ρ = ρ1 ∪ ρ2:1(L11 η1 )ρ = (L11 η1 )ρ1 ,2(L21 η2 )ρ = (L21 η2 )ρ2Òàê êàê L00 = L11η1ρ1 è ¬L00 = ¬L21η2ρ2, âåðíî(L11 η1 )ρ = (L21 η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.

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

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