LectLog10 (1158002), страница 2

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

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

. , L1k1 унифицируемы. Значит, они имеют НОУ η1 ,т. е.η1 ∈ НОУ(L11 , L12 , . . . , L1k1 ),θ1 = η1 ρ1 .Значит D1 η1 — склейка дизъюнкта D1 по литерамL11 , L12 , . . . , L1k1 , и при этом D10 = D1 θ1 = (D1 η1 )ρ1 — основнойпример склейки D1 η2 .Аналогично, литеры ¬L21 , ¬L22 , . . . , ¬L2k2 имеют НОУ η2 .Тогда D2 η2 — склейка дизъюнкта D2 по литерам¬L21 , ¬L22 , . . . , ¬L2k2 , и при этом D20 = D2 θ2 = (D1 η2 )ρ2 —основной пример склейки D2 η2 .ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеb 2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2@@η2b 1 ∨ L11 ∨ · · · ∨ L1kD1@ @η1@ @@R @R@b 1 η1 ∨ L11 η1 = D1 η1Dρ1?@R@??b 0 ∨ L0 = D1 η1 ρ1D10@@@@R@b0 ∨ Db0D12R@b 2 η2 ¬ ∨ L21 η2 = D2 η2Dρ2?b 0 ∨ ¬L0 = D2 η2 ρ2D20ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеСогласно нашей привычке переименовывать переменные,дизъюнкты-склейки D1 η1 и D2 η2 содержат разные наборыпеременных.

Поэтому Domρ1 ∩ Domρ2 = ∅, и существуетподстановка ρ = ρ1 ∪ ρ2 :(L11 η1 )ρ = (L11 η1 )ρ1 ,(L21 η2 )ρ = (L21 η2 )ρ2L00Так как= L11 η1 ρ1 и ¬L00 = ¬L21 η2 ρ2 , верно(L11 η1 )ρ = (L21 η2 )ρ, т. е. литеры L11 η1 и L21 η2 унифицируемы.Значит, они имеют НОУ λ, т. е.λ ∈ НОУ(L11 η1 , L21 η2 ), ρ = λµ.b 1 η1 ∨ L11 η1 иПоэтому дизъюнкты-склейки D1 η1 = Db 2 η2 ∨ ¬L21 η2 имеют резольвенту D0 = (Db 1 η1 ∨ Db 2 η2 )λ,D2 η2 = Dи при этомb0 ∨ Db0 = Db 1 η1 ρ ∨ Db 2 η2 ρ = (Db 1 η1 ∨ Db 2 η2 )λµ = D0 µ.D00 = D12ПОЛНОТА РЕЗОЛЮТИВНОГО ВЫВОДАДоказательство леммы о подъемеb 2 ∨ ¬L21 ∨ · · · ∨ ¬L2kD2@@η2b 1 ∨ L11 ∨ · · · ∨ L1kD1@ @η1@ @@R @R@@R@R@b 1 η1 ∨ L11 η1 = D1 η1b 2 η2 ∨ ¬L21 η2 = D2 η2DDXXXXXρλ ρXz X9b 1 η1 ∨ Db 2 η2 )λ?(D?000bbD1 ∨ L0 = D1 η1 ρD2 ∨ ¬L00 = D2 η2 ρ@µ@@@R?@b0 ∨ 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 )D1= L(Даша, Саша)θ2 = {y1 /Саша}D20 = ¬L(Паша, Саша)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 )D1= L(Даша, Саша)θ2 = {y1 /Саша}D20 = ¬L(Паша, Саша)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 )D2 = L(Саша, пиво)θ4 = {y2 /пиво}D40= ¬L(Паша, пиво)ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD30 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )D2 = L(Саша, пиво)θ4 = {y2 /пиво}D40= ¬L(Паша, пиво)D3 = L(Паша, пиво)ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD30 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )D2 = L(Саша, пиво)θ4 = {y2 /пиво}D40= ¬L(Паша, пиво)D3= L(Паша, пиво)θ2 = εD50 = ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙРешение задачи.6. Линейный резолютивный выводD30 = ¬L(Паша, y2 ) ∨ ¬L(Саша, y2 )D2 = L(Саша, пиво)θ4 = {y2 /пиво}D40= ¬L(Паша, пиво)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..

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

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