Ещё одни лекции В.А. Захарова, страница 15

Сводим проблему логического следования{ϕ1 , ϕ2 , ϕ3 , ϕ4 } |= ϕ0к проблеме общезначимости|= ϕ1 & ϕ2 & ϕ3 & ϕ4 → ϕ0 .2. Сводим проблему общезначимости к проблемепротиворечивостиψ1 = ¬ (ϕ1 & ϕ2 & ϕ3 & ϕ4 → ϕ0 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.3. Строим предваренную нормальную форму ПНФL(Саша, пиво) &ψ2 = ∀x∀y ∀zL(Саша, пиво) &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. А теперь будем строить резолютивный вывод.Будем руководствоваться такой стратегией:Начнем с дизъюнкта-запроса D0 ;На каждом шаге вывода будем использовать последнююиз построенных резольвент (линейный вывод ).ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6.

Линейный резолютивный выводD0 = ¬L(z, Даша)ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD0 = ¬L(z, Даша)D4 = ¬L(Паша, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Паша, x1 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD0 = ¬L(z, Даша)D4 = ¬L(Паша, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Паша, x1 )θ1 = {z/Паша, x1 /Даша}D1 = ¬L(Паша, y1 ) ∨ ¬L(Даша, y1 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD0 = ¬L(z, Даша)D4 = ¬L(Паша, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Паша, x1 )θ1 = {z/Даша, x1 /Даша}D1 = ¬L(Паша, y1 ) ∨ ¬L(Даша, y1 )D1 = L(Даша, Саша)ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6.

Линейный резолютивный выводD0 = ¬L(z, Даша)D4 = ¬L(Паша, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Паша, x1 )θ1 = {z/Даша, x1 /Даша}D1 = ¬L(Паша, y1 ) ∨ ¬L(Даша, y1 ) D1= L(Даша, Саша)θ2 = {y1 /Саша}D2 = ¬L(Паша, Саша)ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD0 = ¬L(z, Даша)D4 = ¬L(Паша, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Паша, x1 )θ1 = {z/Даша, x1 /Даша}D1 = ¬L(Паша, y1 ) ∨ ¬L(Даша, y1 )D1 = L(Даша, Саша)θ2 = {y1 /Саша}D2 = ¬L(Паша, Саша)D4 = ¬L(Паша, y2 ) ∨ ¬L(x2 , y2 ) ∨ L(Паша, x2 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD0 = ¬L(z, Даша)D4 = ¬L(Паша, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Паша, x1 )θ1 = {z/Даша, x1 /Даша}D1 = ¬L(Паша, y1 ) ∨ ¬L(Даша, y1 )D1 = L(Даша, Саша)θ2 = {y1 /Саша}D2 = ¬L(Паша, Саша) D4 = ¬L(Паша, y2 ) ∨ ¬L(x2 , y2 ) ∨ L(Паша, x2 )θ3 = {x2 /Саша}D3 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6.

Линейный резолютивный выводD0 = ¬L(z, Даша)D4 = ¬L(Паша, y1 ) ∨ ¬L(x1 , y1 ) ∨ L(Паша, x1 )θ1 = {z/Даша, x1 /Даша}D1 = ¬L(Паша, y1 ) ∨ ¬L(Даша, y1 )D2 = ¬L(Паша, Саша)D1 = L(Даша, Саша)θ2 = {y1 /Саша}D4 = ¬L(Паша, y2 ) ∨ ¬L(x2 , y2 ) ∨ L(Паша, x2 )θ3 = {x2 /Саша}D3 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD3 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6.

Линейный резолютивный выводD3 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )D2 = L(Саша, пиво)ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD3 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )D2 = L(Саша, пиво)θ4 = {y2 /пиво}D4 = ¬L(Паша, пиво)ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD3 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )D2 = L(Саша, пиво)θ4 = {y2 /пиво}D4 = ¬L(Паша, пиво)D3 = L(Паша, пиво)ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD3 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )D4 = ¬L(Паша, пиво)D5 = D2 = L(Саша, пиво)θ4 = {y2 /пиво}D3 = L(Паша, пиво)θ2 = εПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6.

Линейный резолютивный выводD3 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )D4 = ¬L(Паша, пиво)D2 = L(Саша, пиво)θ4 = {y2 /пиво}D3 = L(Паша, пиво)θ5 = εD5 = Успешный резолютивныйвывод завершен!ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.Итак, система дизъюнктов 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 |= D}.Наложим ограничение на применение правила резолюции:При построении резольвенты, оба дизъюнкта-предпосылкидолжны принадлежать разным множествам S1 и S2 .D1 = D1 ∨ L1 , D2 = D2 ∨ ¬L2, D1 ∈ S1I , D2 ∈ S2I , θ ∈ НОУ(L1 , L2 ).D0 = (D1 ∨ D2 )θТакое правило будем называть правилом I -резолюции .СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАПример.Пусть I = ∅, т.

е. I |= P, I |= Q, I |= 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;D4 + D3 = Q;D1 + D3 = ¬P ∨ R;(D1 + D2 ) + D3 = R;((D1 + D2 ) + D3 ) + D4 = СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАТеорема полноты I -резолюцииЕсли система дизъюнктов S противоречива, то для любойинтерпретации I существует успешный I -резолютивный выводпустого дизъюнкта из S.Доказательство:Самостоятельно.СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАЛинейная резолюцияПредположим, что в системе дизъюнктов S выделен некоторыйдизъюнкт D0 .Тогда резолютивный вывод пустого дизъюнкта из системыдизъюнктов S можно строить, руководствуясь следующимисоглашениями:Для построения первой резольвенты D1 выбираетсядизъюнкт D0 и некоторый дизъюнкт D ∈ S \ {D0 };Для построения 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 = .СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАТеорема полноты линейного резолютивноговыводаЕсли система дизъюнктов S противоречива, а системадизъюнктов S = S \ {D0 } непротиворечива, то существуетуспешный линейный резолютивный вывод пустого дизъюнкта из S.Доказательство:Самостоятельно.СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДААвтоматические пруверыfor1stThe World ChampionshipOrder Automated Theorem ProvingVampire (Manchester, A.

Voronkov),SPASS (Max Plank Institute, M. Keil),SNARK (AIC, California, E. Stikel),Otter (Argonne National Laboratory, USA, W. McCune),Gandalf (Goteborg, Tartu, T. Tammet),Carine (Montreal, Quebec, P. Haraoun).РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯМетод резолюций можно использовать для решения разныхзадач. Например, для получения ответа на вопросА будет ли утверждение ϕ0 обязательно верно,если известно, что верны утверждения ϕ1 , ϕ2 , .

. . , ϕn ?Здесь ϕ1 , ϕ2 , . . . , ϕn — это база знаний , ϕ0 — это запрос .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯМатематическая постановка задачи такова: проверить{ϕ1 , ϕ2 , . . . , ϕn } |= ϕ0 .Проверка логического следствия сводится к проверкеобщезначимости: |= (ϕ1 &ϕ2 & . . . &ϕn ) → ϕ0 .Проверка общезначимости сводитсяк проверкепротиворечивости формулы ¬ (ϕ1 &ϕ2 & . .