Лекции В.А. Захарова (1157993), страница 21
Текст из файла (страница 21)
. . &Cn0⇐⇒множество дизъюнктов {D1 , D2 , . . . , DN , ¬C10 ∨¬C2 ∨. . .∨¬Cn0 }противоречиво.⇐⇒ (по теореме Эрбрана)существует такое конечное множество основных примеров0 } ⊆ [P], чтопрограммных утверждений {D10 , D20 , . . . , DM000множество дизъюнктов {D1 , D2 , . . . , DM , ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0 }противоречиво.⇐⇒ (по теореме полноты метода резолюций)0 , ¬C 0 ∨¬C 0 ∨. . .∨¬C 0 }из системы дизъюнктов {D10 , D20 , . .
. , DMn12резолютивно выводим пустой дизъюнкт .ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , . . . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.негативные дизъюнктысмешанные дизъюнктыD10 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1D20 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2...0 =ADM∨0M ¬A1M ∨ · · · ∨ ¬A`MG00 = ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , .
. . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.негативные дизъюнктысмешанные дизъюнктыD10 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1D20 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2...0 =ADM∨0M ¬A1M ∨ · · · ∨ ¬A`MG00 = ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , .
. . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.негативные дизъюнктысмешанные дизъюнктыD10 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1G00 = ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0D20 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2...0 =ADM∨0M ¬A1M ∨ · · · ∨ ¬A`Mвозможны резольвенты двух типовЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , .
. . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.негативныедизъюнктысмешанные дизъюнктыD10 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1 - uG00 = ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0@D20 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2@...@ Это SLD-резольвента0 =ADM@0M ∨ ¬A1M ∨ · · · ∨ ¬A`M@возможны резольвенты двух типов@R@¬A11∨. . .∨¬Ak1∨¬C20∨. . .∨¬Cn0ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , .
. . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.негативные дизъюнктысмешанные дизъюнктыD10 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak10G00 = ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0D2 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2?u... 0 =ADM0M ∨ ¬A1M ∨ · · · ∨ ¬A`Mвозможны резольвенты двух типов@@А это не SLD-резольвента@R@¬A11∨.
. .∨¬Ak1∨¬C20∨. . .∨¬Cn0A02∨¬A22∨. . .∨¬Ar 2∨¬A11∨. . .∨¬Ak1ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , . . . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.негативные дизъюнктысмешанные дизъюнктыD10 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1G00 = ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0D20 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2...0 =ADM∨0M ¬A1M ∨ · · · ∨ ¬A`Mвозможны резольвенты двух типов¬A11∨. . .∨¬Ak1∨¬C20∨. .
.∨¬Cn0A02∨¬A22∨. . .∨¬Ar 2∨¬A11∨. . .∨¬Ak1ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ),ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cm0A00 ∨ ¬A01 ∨ · · · ∨ ¬A0kHHHHjA000 ∨ ¬A001 ∨ · · · ∨ ¬A00rA00 ∨ ¬A02 ∨ · · · ∨ ¬A0k ∨ ¬A001 ∨ · · · ∨ ¬A00rЕсли правило резолюции вначале применяетсяк двум программным утверждениям,ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты.
В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cm0A00 ∨ ¬A01 ∨ · · · ∨ ¬A0kA000 ∨ ¬A001 ∨ · · · ∨ ¬A00rH HHHjA0 ∨ ¬A0 ∨ · · · ∨ ¬A0k ∨ ¬A001 ∨ · · · ∨ ¬A00rXX0 2XXXXXz?¬A02 ∨ · · · ∨ ¬A0k ∨ ¬A001 ∨ · · · ∨ ¬A00r ∨ ¬C20 ∨ · · · ∨ ¬Cm0а затем применяется к полученной резольвенте и запросу,ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты.
В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cm0A00 ∨ ¬A01 ∨ · · · ∨ ¬A0kA000 ∨ ¬A001 ∨ · · · ∨ ¬A00rHHHHHHj?H¬A01 ∨ ¬A02 ∨ · · · ∨ ¬A0k ∨ ¬C2 ∨ · · · ∨ ¬Cmто изменим порядок применения правилЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты.
В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cm0A00 ∨ ¬A01 ∨ · · · ∨ ¬A0kHHHA000 ∨ ¬A001 ∨ · · · ∨ ¬A00rHHHHHHHj?H00 ∨ · · · ∨ ¬A0 ∨ ¬C ∨ · · · ∨ ¬CH2mHH ¬A1 ∨ ¬A2kHjH¬A02 ∨ · · · ∨ ¬A0k ∨ ¬A001 ∨ · · · ∨ ¬A00r ∨ ¬C20 ∨ · · · ∨ Cm0и получим тот же самый результат,но уже только при помощи SLD-резолюции.ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство.Будем применять этот прием, до тех пор пока в выводе неостанутся только правила SLD-резолюции.
Таким образом, витоге получим вывод пустого дизъюнкта из множествадизъюнктов{D1 , D2 , . . . , DN , ¬C10 ∨¬C2 ∨· · · ∨¬Cn0 }только при помощи правила SLD-резолюции.Это и есть успешное SLD-резолютивное вычисление основногозапроса G00 =?C10 , C20 , .
. . Cn0 , обращенного к множеству основныхпримеров программных утверждений [P].Что и требовалось доказать.ЛЕММА О ПОДЪЕМЕЛемма о подъеме (для логических программ)Пусть G00 = G0 θ0 — основной пример запроса G0 с множествомцелевых переменных Y1 , . . . , Ym , обращенный к хорновскойлогической программе P.Если запрос G00 , обращенный к множеству основных примеровпрограммных утверждений [P], имеет успешное вычисление,то исходный запрос G0 , обращенный к самой программе P,также имеет успешное вычисление с ответом η, которыйудовлетворяет равенствуθ0 = ηρ0для некоторой подстановки ρ0 .ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеРассмотрим SLD-резолютивное вычисление запроса G00 = G0 θ0с использованием основных примеров программныхутверждений из множества [P](D10 , ε, G10 ), (D20 , ε, G20 ), .
. . , (Dn0 , ε, )и покажем, что существует SLD-резолютивное вычислениезапроса G0 с использованием программы P(D1 , η1 , G1 ), (D2 , η2 , G2 ), . . . , (Dn , ηn , ),удовлетворяющее условиям леммы.ЛЕММА О ПОДЪЕМЕG0ЛЕММА О ПОДЪЕМЕG0θ0?G0 θ0ЛЕММА О ПОДЪЕМЕG0D1θ0?G0 θ0D2µ1Dnµ2D10?D20AAAµn?ε AAU G 01εAAU G0A2?Dn0qqq0Gn−1AεAA-AU ЛЕММА О ПОДЪЕМЕ- G1G0η1D1θ0?G0 θ0q- G2qqGn−1η2ηnD2µ1Dnµ2D10?D20AAAµn?ε AAU G 01- εAAU G0A2?Dn0qqq0Gn−1AεAA-AU ЛЕММА О ПОДЪЕМЕ- G1G0η1D1θ0?G0 θ0q- G2qqGn−1η2ηnD2µ1Dnµ2D10?D20AAAµn?ε AAU G 01- εAAU G0A2?Dn0qqq0Gn−1θ0 = (η1η2 . . .
ηn)|Y1,...,Ym ρ0AεAA-AU ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1θ00µ1?G00?= G0θ0D10@@@@R@G10= D1 µ1ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1@@@θ00η1µ1@R@?G00= G0θ0G1@@@@R@G10?D10= D1 µ1ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1@@@θ00η1µ1@R@?G00= G0θ0G1?D10= D1 µ1ρ1@@@@R?@G10 = G1 ρ1ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1@@@θ00η1µ1@R@?G00= G0θ0G1?D10= D1 µ1ρ1@@@@R?@G10 = G1 ρ1И при этом верно равенство θ00 = (η1 ρ1 )|Y1 ,...,Ym .ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеПоследовательно применяя этот прием на всех шагахвычисления запроса G00 , получаем SLD-резолютивноевычисление запроса G0 :(D1 , η1 , G1 ), (D2 , η1 , G2 ), .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
