Лекции 12-23. Математическая логика (после колка) (1161871), страница 4
Текст из файла (страница 4)
. &Cm )θ1 θ0следуетP |= ∀Z (A1 & . . . &Ar )θ1 θ0 .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеP |= ∀Z (A1 & . . . &Ar )θ1 θ0 → A0 θ1 θ0 .Таким образом,P |= ∀Z A0 θ1 θ0 .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . . . &A1 & . .
. &Ar & . . . &Cm )θ1 θ0следуетP |= ∀Z (A1 & . . . &Ar )θ1 θ0 .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеP |= ∀Z (A1 & . . . &Ar )θ1 θ0 → A0 θ1 θ0 .Таким образом,P |= ∀Z A0 θ1 θ0 .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Итак, из P |= ∀Z (C1 &C2 & . .
. &A1 & . . . &Ar & . . . &Cm )θ1 θ0следуетP |= ∀Z (C1 & . . . &Ci−1 &Ci+1 & . . . Cm )θ1 θ0 .Мы показали, чтоP |= ∀Z Ci θ1 θ0 .Значит,P |= ∀Z (C1 & . . . &Ci−1 &Ci &Ci+1 & . . . Cm ) θ1 θ0 .{z} |{z}|G0θЗначит, θ1 θ0 |VarG0 = (θ1 θ2 . . . θn )|Y1 ,Y2 ,...,Yk = θ — правильныйответ на запрос G0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИИтак, всякий вычисленный ответ — правильный.А можно ли вычислить любой правильный ответ?Полна ли наша операционная семантика?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММПроблема полнотыПусть θ — правильный ответ на запрос G0 к хорновскойлогической программе P, т. е.
P |= ∀Z G0 θ.Существует ли такое успешное SLD-резолютивное вычисление,порожденное запросом G0 к программе P(Dj1 , η1 , G1 ), (Dj2 , η2 , G2 ), . . . , (Djn , ηn , ),которое вычисляет ответ θ, т. е. θ = (η1 η2 . . . ηn )|VarG0 ?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММТеорема полноты.ПустьP = {D1 , D2 , .
. . , DN } — хорновская логическая программа,G0 =?C1 , C2 , . . . Cm — запрос с множеством целевыхпеременных Y1 , Y2 , . . . , Yk ,θ — правильный ответ на запрос G0 к хорновскойлогической программе P.Тогда существует такой вычисленный ответ η на запрос G0 кпрограмме P, чтоθ = ηρдля некоторой подстановки ρ.Теорема полноты гласит, что каждый правильный ответ — этопример (частный случай) некоторого вычисленного ответа .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММДоказательство.Пусть θ = {Y1 /t1 , .
. . , Yk /tk } и пустьkSVarti = {Z1 , . . . , Zr }.i=1Выберем некоторое множество новых «свежих» констант{c1 , . . . , ck }, не содержащихся ни в программе P, ни взапросе G , ни в термах подстановки θ, и рассмотримподстановку λ = {Z1 /c1 , Z2 /c2 , . . . , Zr /cr }.Поскольку θ — правильный ответ, верно P |= ∀Z1 . . . ∀Zk G0 θ.Запрос G00 = G0 θλ — основной пример запроса G0 , и поэтомуP |= G0 θλ.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММДоказательство.Общий замысел доказательства1. Вначале покажем, что запрос G00 = G0 θλ, обращенный кмножеству [P] основных примеров программных утвержденийпрограммы P, имеет успешное SLD-резолютивное вычисление(лемма об основных вычислениях ).2.
Затем покажем, что исходный запрос G0 , обращенный ксамой программе P, имеет успешное SLD-резолютивноевычисление с таким вычисленным ответом η, для котороговерно равенство θλ = ηρ0 для некоторой подстановки ρ0(лемма о подъеме для хорновских дизъюнктов ).3. Затем покажем, что отсюда следует равенство θ = ηρ длянекоторой подстановки ρ.ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХЛемма об основных вычислениях.ПустьP = {D1 , D2 , . . .
, DN } — хорновская логическая программа,G00 =?C10 , C20 , . . . Cn0 — основной запрос,и при этом верно P |= G00 .Тогда существует успешное SLD-резолютивное вычислениезапроса G00 , обращенного к множеству [P] основных примеровпрограммных утверждений программы P.ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.{D1 , D2 , . . . , DN } |= C10 &C20 & . . . &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-резольвенты.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
