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

, DMn12резолютивно выводим пустой дизъюнкт .ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы , ¬C ∨ ¬C ∨ · · · ∨ ¬C }.{D1 , D2 , . . . , DMn12Но это не обязательно SLD-резолютивный вывод.

Рассмотримего более подробно.смешанные дизъюнктынегативные дизъюнктыD1 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1D2 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2... =A∨DM0M ¬A1M ∨ · · · ∨ ¬AMG0 = ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CnЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы , ¬C ∨ ¬C ∨ · · · ∨ ¬C }.{D1 , D2 , .

. . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.смешанные дизъюнктынегативные дизъюнктыD1 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1D2 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2... =A∨DM0M ¬A1M ∨ · · · ∨ ¬AMG0 = ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CnЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы , ¬C ∨ ¬C ∨ · · · ∨ ¬C }.{D1 , D2 , .

. . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.смешанные дизъюнктынегативные дизъюнктыD1 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1G0 = ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CnD2 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2... =A∨DM0M ¬A1M ∨ · · · ∨ ¬AMвозможны резольвенты двух типовЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы , ¬C ∨ ¬C ∨ · · · ∨ ¬C }.{D1 , D2 , . . . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.смешанные дизъюнктынегативныедизъюнктыD1 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1 - uG0 = ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cn@D2 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2@...@ Это SLD-резольвента =A@DM0M ∨ ¬A1M ∨ · · · ∨ ¬AM@возможны резольвенты двух типов@R@¬A11∨.

. .∨¬Ak1∨¬C2∨. . .∨¬CnЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы , ¬C ∨ ¬C ∨ · · · ∨ ¬C }.{D1 , D2 , . . . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.смешанные дизъюнктынегативные дизъюнктыD1 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1 G0 = ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CnD2 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2?u...

=ADM0M ∨ ¬A1M ∨ · · · ∨ ¬AMвозможны резольвенты двух типов@@А это не SLD-резольвента@R@¬A11∨. . .∨¬Ak1∨¬C2∨. . .∨¬CnA02∨¬A22∨. . .∨¬Ar 2∨¬A11∨. . .∨¬Ak1ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы , ¬C ∨ ¬C ∨ · · · ∨ ¬C }.{D1 , D2 , . . .

, DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.смешанные дизъюнктынегативные дизъюнктыD1 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1G0 = ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CnD2 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2... =A∨DM0M ¬A1M ∨ · · · ∨ ¬AMвозможны резольвенты двух типов¬A11∨. . .∨¬Ak1∨¬C2∨.

. .∨¬CnA02∨¬A22∨. . .∨¬Ar 2∨¬A11∨. . .∨¬Ak1ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ),ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты.

В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CmA0 ∨ ¬A1 ∨ · · · ∨ ¬AkHHHH jA0 ∨ ¬A1 ∨ · · · ∨ ¬ArA0 ∨ ¬A2 ∨ · · · ∨ ¬Ak ∨ ¬A1 ∨ · · · ∨ ¬ArЕсли правило резолюции вначале применяетсяк двум программным утверждениям,ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CmA0 ∨ ¬A1 ∨ · · · ∨ ¬AkA0 ∨ ¬A1 ∨ · · · ∨ ¬ArH HHjHA ∨ ¬A ∨ · · · ∨ ¬Ak ∨ ¬A1 ∨ · · · ∨ ¬ArXXX0 2XXXz?X¬A2 ∨ · · · ∨ ¬Ak ∨ ¬A1 ∨ · · · ∨ ¬Ar ∨ ¬C2 ∨ · · · ∨ ¬Cmа затем применяется к полученной резольвенте и запросу,ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты.

В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CmA0 ∨ ¬A1 ∨ · · · ∨ ¬AkA0 ∨ ¬A1 ∨ · · · ∨ ¬ArHHHHHHHj?¬A1 ∨ ¬A2 ∨ · · · ∨ ¬Ak ∨ ¬C2 ∨ · · · ∨ ¬Cmто изменим порядок применения правилЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CmA0 ∨ ¬A1 ∨ · · · ∨ ¬AkA0 ∨ ¬A1 ∨ · · · ∨ ¬ArHHHHHHHHHHHHj?H¬A ∨ ¬A ∨ · · · ∨ ¬Ak ∨ ¬C2 ∨ · · · ∨ ¬Cm12HHjH¬A2 ∨ · · · ∨ ¬Ak ∨ ¬A1 ∨ · · · ∨ ¬Ar ∨ ¬C2 ∨ · · · ∨ Cmи получим тот же самый результат,но уже только при помощи SLD-резолюции.ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство.Будем применять этот прием, до тех пор пока в выводе неостанутся только правила SLD-резолюции.

Таким образом, витоге получим вывод пустого дизъюнкта из множествадизъюнктов{D1 , D2 , . . . , DN , ¬C1 ∨¬C2 ∨· · · ∨¬Cn }только при помощи правила SLD-резолюции.Это и есть успешное SLD-резолютивное вычисление основногозапроса G0 =?C1 , C2 , . . .

Cn , обращенного к множеству основныхпримеров программных утверждений [P].Что и требовалось доказать.ЛЕММА О ПОДЪЕМЕЛемма о подъеме (для логических программ)Пусть G0 = G0 θ — основной пример запроса G0 с множествомцелевых переменных Y1 , . . . , Ym , обращенный к хорновскойлогической программе P.Если запрос G0 , обращенный к множеству основных примеровпрограммных утверждений [P], имеет успешное вычисление,то исходный запрос G0 , обращенный к самой программе P,также имеет успешное вычисление с ответом η, которыйудовлетворяет равенствуθ = ηρдля некоторой подстановки ρ .ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеРассмотрим SLD-резолютивное вычисление запроса G0 = G0 θс использованием основных примеров программныхутверждений из множества [P](D1 , ε, G1 ), (D2 , ε, G2 ), .

. . , (Dn , ε, )и покажем, что существует SLD-резолютивное вычислениезапроса G0 с использованием программы P(D1 , η1 , G1 ), (D2 , η2 , G2 ), . . . , (Dn , ηn , ),удовлетворяющее условиям леммы.ЛЕММА О ПОДЪЕМЕG0ЛЕММА О ПОДЪЕМЕG0θ?G0 θЛЕММА О ПОДЪЕМЕG0D1θD2μ1?μn?D2ADnAAG0 θμ2?D1?Dnε A-AU G 1εAA-AU G2AqqqGn−1εAA-AU ЛЕММА О ПОДЪЕМЕ- G1G0- G2η1D1θqη2μ1?μ2μn?DnAε A-AU G 1εAA-AU G2ηnDn?A- Gn−1D2AG0 θqD2D1?qAqqqGn−1εAA-AU ЛЕММА О ПОДЪЕМЕ- G1G0- G2η1D1θqη2μ1μn??DnAAε A-AU G 1εAA-AU G2ηnDnD2A- Gn−1μ2?G0 θqD2D1?qAqqqGn−1θ = (η1η2 . . . ηn)|Y1,...,Ym ρεAA-AU ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1θ0G0μ1?= G0θD1@@@@R@G1?= D1 μ1ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1@@@θ0G0?= G0θη1@R@G1@@@@R@G1μ1D1?= D1 μ1ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0@θ0G0D1@@@?= G0θη1@RG1ρ1@@μ1D1?= D1 μ1@@R?@G1 = G1 ρ1ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0@θ0G0D1@@@?= G0θη1@RG1ρ1@@μ1D1?= D1 μ1@@R?@G1 = G1 ρ1И при этом верно равенство θ0 = (η1 ρ1 )|Y1 ,...,Ym .ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеПоследовательно применяя этот прием на всех шагахвычисления запроса G0 , получаем SLD-резолютивноевычисление запроса G0 :(D1 , η1 , G1 ), (D2 , η1 , G2 ), .

. . , (Dn , ηn , )для которого выполняется система равенствθ = (η1 ρ1 )|Y1 ,...,Ymρ1 = (η2 ρ2 )|VarG1ρ2 = (η3 ρ3 )|VarG2...ρn = (ηn ρn )|VarGnИз этой системы следует равенство θ = (η1 η2 . . . ηn )|Y1 ,...,Ym ρдля некоторой подстановки ρ .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство теоремы полноты (завершение).Итак, у нас естьправильный ответ θ0 на запрос G0 к хорновскойлогической программе P;подстановка λ = {Z1 /c1 , Z2 /c2 , . .

. , Zr /cr } «свежих»констант на место всех переменных Z1 , . . . , Zr из термовподстановки θ0 .основной пример θ0 = θ0 λ правильного ответа θ.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство теоремы полноты (завершение).θ0 — правильный ответ на запрос G0 к хорновской логическойпрограмме P;⇓P |= G0 θ0 λ;⇓(по лемме об основных вычислениях )основной запрос G0 θ0 λ к множеству основных примеровпрограммных утверждений [P] имеет успешное вычисление;⇓(по лемме о подъеме для логических программ )запрос G0 к программе P имеет успешное вычисление свычисленным ответом η, для которого верно равенствоθ0 λ = ηρдля некоторой подстановки ρ .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство теоремы полноты (завершение).А теперь заменим в левой и правой частях равенстваθ0 λ = ηρвсе константы c1 , .

. . , cr на символы переменных Z1 , . . . , Zr .Поскольку константы c1 , . . . , cr не входят в состав запроса G0 ипрограммы P, эти константы не входят в состав термоввычисленного ответа η, и, значит, могут содержаться только вподстановке ρ .В левой части равенства подстановка λ = {Z1 /c1 , . . . , Zr /cr }превращается в пустую подстановку ε.В правой части равенства подстановка ρ превращается внекоторую новую подстановку ρ.В итоге равенство θ0 λ = ηρ превращается в равенствоθ0 = ηρПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИПоясняющий пример.Рассмотрим запрос ?P(U, V ) к логической программеP : P(f (X ), X ) ← R(X ); (1)R(Y ) ←;(2)Q(c) ←;(3)Легко видеть, что θ = {U/f (c), V /c} — это правильный ответна запрос к программе.Вместе с тем, единственный вычисленный ответ — этоη = {U/f (Y ), V /Y }.Все дело в том, что θ — это частный случай η: θ = η{Y /c}.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИИтак, любой правильный ответ на запрос к хорновскойлогической программе можно вычислить (возможно, собобщением) по правилу SLD-резолюции, и любойвычисленный ответ будет правильным.А как организовать вычисления логических программ, чтобывычислить ВСЕ ответы?КОНЕЦ ЛЕКЦИИ 13.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.