Лекции 12-23. Математическая логика (после колка) (1161871), страница 5
Текст из файла (страница 5)
В этом выводе обязательноесть хотя бы одна 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 ), .
. . , (Dn , ηn , )для которого выполняется система равенствθ0 = (η1 ρ1 )|Y1 ,...,Ymρ1 = (η2 ρ2 )|VarG1ρ2 = (η3 ρ3 )|VarG2...ρn = (ηn ρn )|VarGnИз этой системы следует равенство θ0 = (η1 η2 . . . ηn )|Y1 ,...,Ym ρ0для некоторой подстановки ρ0 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство теоремы полноты (завершение).Итак, у нас естьIправильный ответ θ0 на запрос G0 к хорновскойлогической программе P;Iподстановка λ = {Z1 /c1 , Z2 /c2 , . . .
, Zr /cr } «свежих»констант на место всех переменных Z1 , . . . , Zr из термовподстановки θ0 .Iосновной пример θ00 = θ0 λ правильного ответа θ.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство теоремы полноты (завершение).θ0 — правильный ответ на запрос G0 к хорновской логическойпрограмме P;⇓P |= G0 θ0 λ;⇓(по лемме об основных вычислениях )основной запрос G0 θ0 λ к множеству основных примеровпрограммных утверждений [P] имеет успешное вычисление;⇓(по лемме о подъеме для логических программ )запрос G0 к программе P имеет успешное вычисление свычисленным ответом η, для которого верно равенствоθ0 λ = ηρ0для некоторой подстановки ρ0 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство теоремы полноты (завершение).А теперь заменим в левой и правой частях равенстваθ0 λ = ηρ0все константы c1 , . .
. , cr на символы переменных Z1 , . . . , Zr .Поскольку константы c1 , . . . , cr не входят в состав запроса G0 ипрограммы P, эти константы не входят в состав термоввычисленного ответа η, и, значит, могут содержаться только вподстановке ρ0 .В левой части равенства подстановка λ = {Z1 /c1 , . . . , Zr /cr }превращается в пустую подстановку ε.В правой части равенства подстановка ρ0 превращается внекоторую новую подстановку ρ.В итоге равенство θ0 λ = ηρ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.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.
ЗахаровЛекция 14.Правила выбора подцелей.Деревья вычислений логическихпрограмм.Стратегии вычисления логическихпрограмм.ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙSLD-резолютивное вычисление запроса ?G к логическойпрограмме P определяется неоднозначно.Рассмотрим запрос ?P(U, V ), R(U) к логической программеP : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;(1)(2)(3)(4)Уже на первом шаге вычисления возникают вопросы выбора:I Какую подцель выделить??P(U, V ), R(U)I?P(U, V ), R(U)Если выделена, например, первая подцель ?P(U, V ), R(U),то какое программное утверждение выбрать?P(X , Y ) ← R(X ), Q(Y ); (1)P(X , X ) ← Q(X );(2)P(X , Y ) ← R(X ), Q(Y ); (1)P(X , X ) ← Q(X );(2)ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙРассмотрим два вычисления запроса ?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)P(X1 , Y1 ) ← R(X1 ), Q(Y1 )R(b) ←θ1 = {U/X1 , V /Y1 }??R(X1 ), Q(Y1 ), R(X1 )η1 = {U/b}??P(b, V )R(b) ←θ2 = {X1 /b}P(X1 , Y1 ) ← R(X1 ), Q(Y1 )??Q(Y1 ), R(b)Q(c) ←η2 = {X1 /b, V /Y1 }??R(b), Q(Y1 )Q(c) ←θ3 = {Y1 /c}??R(b)R(b) ←η3 = {Y1 /c}??R(b)R(b) ←θ4 = ε??η4 = ε??θ = θ1 θ2 θ3 θ4 |{U,V } = {U/b, V /c}η = η1 η2 η3 η4 |{U,V } = {U/b, V /c}ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙКак видите, мы получаем одинаковые вычисленные ответы вобоих вычислениях независимо от порядка выбора подцелей вцелевых утверждениях.Это случайность или так бывает всегда?С точки зрения операционной семантики программ, запрос —это список задач, которые нужно решить.IДля решения запроса нужно решить все подцели запроса.Значит, результат вычисления не зависит от того порядка,в котором решаются задачи (выбираются подцели).IРешение одной задачи может помочь решить другую.Значит, правильно выбранный порядок решения задачсущественно влияет на эффективность вычислениязапроса.Покажем, что верно первое предположение.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИОпределение.Отображение R, которое сопоставляет каждому непустомузапросу G : ?C1 , C2 , .
. . , Cm одну из подцелей Ci = R(G ) в этомзапросе, называется правилом выбора подцелей .Для заданного правила выбора подцелей R вычислениезапроса G к логической программе P называетсяR-вычислением , если на каждом шаге вычисления очереднаяподцель в запросе выбирается по правилу R.Ответ, полученный в результате успешного R-вычисления,называется R-вычисленным .Возникает вопрос:При каком правиле выбора подцелей R каждый вычисленныйответ оказывется R-вычисленным?ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДля каждого программного утвержденияD : A0 ← A1 , A2 , . . . , An условимся использовать запись D +для обозначения атома A0 , а запись D − — для обозначениясписка атомов A1 , A2 , . .
. , An . В частности, если D — это фактA0 ←, то D − — это пустой список.Выбор обозначений обусловлен тем, что утверждениеD : A0 ← A1 , A2 , . . . , An соответствует дизъюнктуположительная литераz}|{A0∨ ¬A1 ∨ ¬A2 ∨ · · · ∨ ¬An{z}|отрицательные литерыПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИПереключательная лемма.Предположим, что запрос G0 :?C1 , . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
