586 слайдов лекций (1158014), страница 15
Текст из файла (страница 15)
å. ëèòåðû 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.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 11.Стратегии резолютивного вывода.Резолютивный вывод каксредство вычисления.СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАМетод резолюций не предписывает заранее никакогофиксированного порядка применения правил резолюции исклейки для вывода пустого дизъюнкта из противоречивогомножества дизъюнктов.Существуют различные стратегии резолютивного вывода ,налагающие дополнительные ограничения на выборподходящих пар дизъюнктов для получения резольвент.Стратегия резолютивного вывода называется полной , если онапозволяет вывести пустой дизъюнкт из любогопротиворечивого множества дизъюнктов.Рассмотрим пример.СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАПример.ПустьS= { D1D2D3D4= ¬P ∨ ¬Q ∨ R;= P ∨ R;= Q ∨ R;= ¬R}Можно построить много разных резольвент:D1 + D2 = ¬Q ∨ R, D1 + D3 = ¬P ∨ R, D1 + D4 = ¬P ∨ ¬Q,D2 + D4 = P, D3 + D4 = Q, и т.
д.Но как ограничиться только теми, которые действительнонужны для вывода ?СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАСемантическая резолюцияРазделим дизъюнкты на два подмножества по следующемупринципу:выберем H-интерпретацию I и положимS1I = {D : D ∈ S, I |= D},S2I = {D : D ∈ S, I 6|= D}.Наложим ограничение на применение правила резолюции:При построении резольвенты, оба дизъюнкта-предпосылкидолжны принадлежать разным множествам S1I и S2I .D1 = D10 ∨ L1 , D2 = D20 ∨ ¬L2, D1 ∈ S1I , D2 ∈ S2I , θ ∈ НОУ(L1 , L2 ).D0 = (D10 ∨ D20 )θТакое правило будем называть правилом I -резолюцией .СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАПример.Пусть I = ∅, т.
е. I 6|= P, I 6|= Q, I 6|= R. ТогдаS1I : D1 = ¬P ∨ ¬Q ∨ R;D4 = ¬R;S2I : D2 = P ∨ R;D3 = Q ∨ R;I -резольвенты будут строиться так:S1 : D1 + D2 = ¬Q ∨ R; S2 : D4 + D2 = P;D1 + D3 = ¬P ∨ R;D4 + D3 = Q;(D1 + D2 ) + D3 = R;((D1 + D2 ) + D3 ) + D4 = СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАТеорема полноты I -резолюцииЕсли система дизъюнктов S противоречива, то для любойинтерпретации I существует успешный I -резолютивный выводпустого дизъюнкта из S.Доказательство:Самостоятельно.СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАВходная резолюцияПредположим, что в системе дизъюнктов S выделен некоторыйдизъюнкт D0 .Тогда резолютивный вывод пустого дизъюнкта из системыдизъюнктов S можно строить, руководствуясь следующимисоглашениями:IДля построения первой резольвенты D1 выбираетсядизъюнкт D0 и некоторый дизъюнкт D ∈ S \ {D0 };IДля построения i-ой резольвенты Di выбираетсярезольвента Di−1 , построенная на предыдущем шагевывода, и дизъюнкт D ∈ S.Резолютивный вывод такого вида будем называть входнымрезолютивным выводом , инициированным дизъюнктом D0 .СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАПример.ПустьS= { D1 = ¬P ∨ ¬Q ∨ R; D2 = P ∨ R;D3 = Q ∨ R;D4 = ¬R}и выделенный дизъюнкт D0 — это D4 = ¬R.Тогда входной резолютивный вывод будет таким:1.
D4 + D1 = ¬P ∨ ¬Q;2. (D4 + D1 ) + D2 = R ∨ ¬Q;3. ((D4 + D1 ) + D2 ) + D3 = R;4. (((D4 + D1 ) + D2 ) + D3 ) + D4 = .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯМетод резолюций можно использовать для решения разныхзадач. Например, для получения ответа на вопросА будет ли утверждение ϕ0 обязательно верно,если известно, что верны утверждения ϕ1 , ϕ2 , . . . , ϕn ?Здесь ϕ1 , ϕ2 , .
. . , ϕn — это база знаний , ϕ0 — это запрос .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯМатематическая постановка задачи такова: проверить{ϕ1 , ϕ2 , . . . , ϕn } |= ϕ0 .Проверка логического следствия сводится к проверкеобщезначимости: |= (ϕ1 &ϕ2 & . . . &ϕn ) → ϕ0 .Проверка общезначимости сводитсяк проверкепротиворечивости формулы ¬ (ϕ1 &ϕ2 & . . . &ϕn ) → ϕ0 , или,что равносильно, противоречивости системы формулS = {ϕ1 , ϕ2 , . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
