Лекции В.А. Захарова (1157993), страница 16
Текст из файла (страница 16)
Ëèíåéíûé ðåçîëþòèâíûé âûâîä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 , . . . , ϕn , ¬ϕ0 }.Для проверки противоречивости системы S применяем методрезолюций.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯНо метод резолюций позволяет решать и более изощренныезадачи.Пусть имеется база знаний Γ = {ϕ1 , ϕ2 , . . . , ϕn } и запросQ = ϕ0 (x1 , .
. . , xm ).Задача: вычислить значения переменных x1 , . . . , xm , прикоторых запрос Q логически следует из базы знаний Γ.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯРешить эту задачу можно попытаться так:задачу проверки логического следствия{ϕ1 , ϕ2 , . . . , ϕn } |= ∃x1 . . . ∃xm ϕ0 (x1 , . . . , xm ).свести к проверке противоречивости системы формулS = {ϕ1 , ϕ2 , . . . , ϕn , ¬ϕ0 (x1 , . . . , xm )}(здесь x1 , . . .
, xm по умолчанию связаны квантором ∀),построить резолютивное опровержение S, иприменить последовательность унификаторовθ1 , θ2 , . . . , θN , вычисленных по ходу построениярезолютивного вывода, к целевым переменным x1 , . . . , xm :x1 θ 1 θ 2 . . . θ N ,...,xm θ 1 θ 2 . . . θ N .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯЭтот трюк сработал при решении задачи о «любовномквадрате Саша–Даша–Паша–пиво».Попробуем применить его еще раз для решения какой-нибудьдругой вычислительной задачи.Поиск пути в графе.Пусть задан ориентированный граф Γ , в котором выделеныдве вершины u и v .
Требуется найти маршрут из вершины u ввершину v .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.граф Γv3y @@v1yv4v2y6-y@@@@@Ryv5@@R yv@6v7yРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Вначале нужно суметь сформулировать эту задачу на языкелогики предикатов.Граф Γ может быть задан перечнем его вершин и дуг. ВведемIконстанты v1 , v2 , .
. . , vn , . . . для обозначения вершинграфов;Iпредикатный символ Vert (1) для обозначения свойства:«x — вершина графа» ;Iпредикатный символ Arc (2) для обозначения свойства:«hx, y i — дуга графа».Чтобы отличать переменные от констант, в дальнейшемусловимся обозначать переменные ЗАГЛАВНЫМИБУКВАМИ, а константы — прописными буквами.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Тогда граф может быть описан следующим набором формуллогики предикатов.KBΓ =nϕ1 = Vert(v1 ), ψ1 = Arc(v1 , v2 ),ϕ2ϕ3ϕ4ϕ5ϕ6= Vert(v2 ),= Vert(v3 ),= Vert(v4 ),= Vert(v5 ),= Vert(v6 ),ψ2ψ3ψ4ψ5ψ6= Arc(v2 , v3 ),= Arc(v2 , v5 ),= Arc(v3 , v6 ),= Arc(v5 , v4 ),= Arc(v4 , v6 ), oϕ7 = Vert(v7 ), ψ7 = Arc(v6 , v5 ),РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Ориентированный путь в графе — это последовательность(список) дуг. Значит нужно иметь подходящую структуруданных для представления список на языке логики предикатов.Для этого мы введемIспециальную константу nil для обозначения пустогосписка, не содержащего ни одного элемента;Iспециальный функциональный символ (2) дляобозначения двухместной операции присоединенияэлемента x к списку y в качестве заголовка (конструкторсписков )..РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе..При помощи введенных символов nil и определимспециальное множество термов — списки :Iконстанта nil — это список;Iесли t — произвольный терм, а T — список,то терм (t, T ) — это список;Iдругих списков нет..Терм t называтся заголовком , а T — хвостом списка.(t, T ).Чтобы сделать обозначения более естественными, мы будемзаписывать знак двухместной операции между аргументами(инфиксная запись), как это делается для операций +, ×..Таким образом, запись.(t , t ) равносильна записи t .t .1212РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Примеры списковПустой список:nilCписок из одного элемента X :.X nil.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
