LectLog13 (Старые лекции, в целом тоже самое)
Описание файла
Файл "LectLog13" внутри архива находится в папке "Старые лекции, в целом тоже самое". PDF-файл из архива "Старые лекции, в целом тоже самое", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 13.Операционная семантикалогических программ:SLD–резолютивные вычисления.Корректность операционнойсемантики.ОПЕРАЦИОННАЯ СЕМАНТИКАЛОГИЧЕСКИХ ПРОГРАММКонцепция операционной семантикиПод операционной семантикой понимают правила построениявычислений программы.
Операционная семантикаописывает, КАК достигается результат работы программы.Результат работы логической программы — это правильныйответ на запрос к программе. Значит, операционная семантикадолжна описывать метод вычисления правильных ответов.Запрос к логической программе порождает задачу ологическом следствии. Значит, вычисление ответа на запросдолжно приводить к решению эту задачу.Таким методом вычисления может быть разновидностьметода резолюций, учитывающая особенности устройствапрограммных утверждений.ОПЕРАЦИОННАЯ СЕМАНТИКАЛогически предпосылки операционной семантикиЗапрос G (Y1 , . . .
Ym ) =? C1 , C2 , . . . , Cm к логической программеP = {D1 , . . . , DN } порождает задачу о логическом следствии:{D1 , . . . , DN } |= ∃Y1 . . . ∃Ym (C1 &C2 & . . . &Cm ),которая равносильна задаче об общезначимости|= D1 & . . . &DN → ∃Y1 . . . ∃Ym (C1 &C2 & . . . &Cm ),которая равносильна задаче о противоречивости формулы¬(D1 & . . . &DN → ∃Y1 .
. . ∃Ym (C1 &C2 & . . . &Cm ),равносильной формулеD1 & . . . &DN & ∀Y1 . . . ∀Ym (¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cm ),ОПЕРАЦИОННАЯ СЕМАНТИКАЛогически предпосылки операционной семантикиПолученную формулуD1 & . . . &DN & ∀Y1 . . . ∀Ym (¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cm ),можно рассматривать как систему дизъюнктовSP,G = {D1 , . . . , DN , ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cm },и доказывать ее противоречивость методом резолюций.ОПЕРАЦИОННАЯ СЕМАНТИКАЛогические программы и хорновские дизъюнктыКаждому утверждению логической программы сопоставимхорновский дизъюнкт:Правило: D 0 = A0 ← A1 , A2 , . .
. , AnD 0 = A0 ∨ ¬A1 ∨ ¬A2 ∨ · · · ∨ ¬AnФакт: D 00 = AD 00 = AЗапрос: G = ? C1 , C2 , . . . , CmG = ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CmКак это принято у дизъюнктов, предполагается, что всеОПЕРАЦИОННАЯ СЕМАНТИКАЛогические программы и хорновские дизъюнктыМы будем применять специальную стратегию построениярезолютивного вывода:G0Di 1?)G1Di 2?)Gq2qqDi k)?Selection rule driven Linear resolution with Definite clausesSLD-резолюцияSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)ПустьIG = ? C1 , .
. . , Ci , . . . , Cm — целевое утверждение, вкотором выделена подцель Ci ,ID 0 = A00 ← A01 , A02 , . . . , A0n — вариант некоторогопрограммного утверждения, в котором VarG ∩ VarD 0 = ∅,Iθ ∈ НОУ(Ci , A00 ) — наиб. общ. унификатор подцели Ci изаголовка программного утверждения A0 .Тогда запросG 0 = ?(C1 , . . . , Ci−1 , A01 , A02 , . . . , A0n , Ci+1 , . . .
, Cm )θназывается SLD-резольвентой программного утверждения D 0 изапроса G с выделенной подцелью Ci и унификатором θ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , . . . , CmКОММЕНТАРИИ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , . . . , CmКОММЕНТАРИИ.Выделяем подцель в запросе.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , .
. . , CmD = A0 ← A1 , A2 , . . . , An ;КОММЕНТАРИИ.Выбираем программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , . . . , CmD 0 = A00 ← A01 , A02 , . . . , A0n ;КОММЕНТАРИИ.Переименовываем переменные в выбранном утверждении,так чтобы VarD 0 ∩ VarG = ∅.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , .
. . , Ci , . . . , CmD 0 = A00 ← A01 , A02 , . . . , A0n ;θ = НОУ(Ci , A00 )КОММЕНТАРИИ.Вычисляем Наиболее Общий Унификатор.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , . . . , CmD 0 = A00 ← A01 , A02 , . . . , A0n ;9?θ = НОУ(Ci , A00 )G 0 = ? (C1 , . . .
, Ci−1 , A01 , A02 , . . . , A0n , Ci+1 , . . . , Cm )θКОММЕНТАРИИ.Строим SLD-резольвентуSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ¬C1 ∨ · · · ∨ ¬Ci ∨ · · · ∨ ¬CmD 0 = A00 ∨ ¬A01 ∨ ¬A02 ∨ · · · ∨ A0n ;9?θ = НОУ(Ci , A00 )G 0 = (¬C1 ∨· · · ∨¬Ci−1 ∨¬A01 ∨¬A02 ∨ · · · ∨¬A0n ∨¬Ci+1 ∨ · · · ∨¬Cm )θКОММЕНТАРИИ.Действительно, это резольвента двух дизъюнктовSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)КОММЕНТАРИИ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)КОММЕНТАРИИ.Выделяем подцель в запросе.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D = R(Y , X ) ← P(X ), R(c, Y );КОММЕНТАРИИ.Выбираем программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D 0 = R(Y1 , X1 ) ← P(X1 ), R(c, Y1 );КОММЕНТАРИИ.Переименовываем переменные в выбранном утверждении,так чтобы VarD 0 ∩ VarG = ∅.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D 0 = R(Y1 , X1 ) ← P(X1 ), R(c, Y1 );θ = НОУ(R(X ,f (Y )),R(Y1 ,X1 )) = {Y1 /X ,X1 /f (Y )}КОММЕНТАРИИ.Вычисляем Наиболее Общий Унификатор.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D 0 = R(Y1 , X1 ) ← P(X1 ), R(c, Y1 );?9θ = НОУ(R(X ,f (Y )),R(Y1 ,X1 )) = {Y1 /X ,X1 /f (Y )}G 0 = ? (P(X ), P(X1 ), R(c, Y1 ), R(Y , c))θКОММЕНТАРИИ.Строим SLD-резольвентуSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D 0 = R(Y1 , X1 ) ← P(X1 ), R(c, Y1 );?9θ = НОУ(R(X ,f (Y )),R(Y1 ,X1 )) = {Y1 /X ,X1 /f (Y )}G 0 = ? P(X ), P(f (Y )), R(c, X ), R(Y , c)КОММЕНТАРИИ.Вот она.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil)КОММЕНТАРИИ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil)КОММЕНТАРИИ.Выделяем подцель в запросе.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D = R(X nil, Y ) ←;КОММЕНТАРИИ.Выбираем программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D 0 = R(X1 nil, Y1 ) ←;КОММЕНТАРИИ.Переименовываем переменные в выбранном утверждении,так чтобы VarD 0 ∩ VarG = ∅.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D 0 = R(X1 nil, Y1 ) ←;...
.θ = НОУ(R(X , X nil),R(X1 nil, Y1 )) ={X /X1 nil,Y1 /(X1 nil) nil}.КОММЕНТАРИИ.Вычисляем Наиболее Общий Унификатор.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D 0 = R(X1 nil, Y1 ) ←;?9... .θ = НОУ(R(X , X nil),R(X1 nil, Y1 )) ={X /X1 nil,Y1 /(X1 nil) nil}.G 0 = ? ( )θКОММЕНТАРИИ.Строим SLD-резольвентуSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D 0 = R(X1 nil, Y1 ) ←;?9G0 = КОММЕНТАРИИ.Вот она.... .θ = НОУ(R(X , X nil),R(X1 nil, Y1 )) ={X /X1 nil,Y1 /(X1 nil) nil}.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y )КОММЕНТАРИИ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y )КОММЕНТАРИИ.Выделяем подцель в запросе.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D = R(X nil, X ) ←;КОММЕНТАРИИ.Выбираем программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, X1 ) ←;КОММЕНТАРИИ.Переименовываем переменные в выбранном утверждении,SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, Y1 ) ←;..НОУ(R(X , X nil),R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Атомы неунифицируемы!SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, Y1 ) ←;..НОУ(R(X , X nil),R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Значит, SLD-резольвенту нельзя построить.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, Y1 ) ←;..НОУ(R(X , X nil),R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Нужно выделить другую подцель иливыбрать другое программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)ПустьIG0 = ? C1 , C2 , .
. . , Cm — целевое утверждение,IP = {D1 , D2 , . . . , DN } — хорновская логическая программа.Тогда (частичным) SLD-резолютивным вычислением ,порожденным запросом G0 к логической программе Pназывается последовательность троек (конечная илибесконечная)(Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . . , (Djn , θn , Gn ), . . . ,в которой для любого i, i ≥ 1,IDji ∈ P, θi ∈ Subst, Gi — целевое утверждение (запрос);Iзапрос Gi является SLD-резольвентой программногоутверждения Dji и запроса Gi−1 с унификатором θi .SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)Частичное SLD-резолютивное вычислениеcomp = (Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . .
. , (Djk , θn , Gn )называетсяIуспешным вычислением (SLD-резолютивнымопровержением), если Gn = ;Iбесконечным вычислением, если comp — это бесконечнаяпоследовательность;Iтупиковым вычислением, если comp — это конечнаяпоследовательность, и при этом для запроса Gnневозможно построить ни одной SLD-резольвенты.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)ПустьIG0 = ? C1 , C2 , .
. . , Cm — целевое утверждение с целевымипеременными Y1 , Y2 , . . . , Yk ,IP = {D1 , D2 , . . . , DN } — хорновская логическая программа,Icomp = (Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . . , (Djn , θn , ) —успешное SLD-резолютивное вычисление, порожденноезапросом G к программе P.Тогда подстановкаθ = (θ1 θ2 .
. . θn )|Y1 ,Y2 ,...,Yk ,представляющая собой композицию всех вычисленныхунификаторов θ1 , θ2 , . . . , θn , ограниченную целевымипеременными Y1 , Y2 , . . . , Yk ,называется вычисленным ответом на запрос G0 к программе P.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)...G0 =?elem(X , a b c nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );..G1 =?elem(X1 , b c nil)...? elem(X , a b c nil)..
θ1 = {X /X1 , Y1 /a, L1 /b c nil}?SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.. θ1 = {X /X1 , Y1 /a, L1 /b c nil}?...G1 =?elem(X1 , b c nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.. θ1 = {X /X1 , Y1 /a, L1 /b c nil}?...G1 =?elem(X1 , b c nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?.θ2 = {X1 /X2 , Y2 /b, L2 /c nil}.G2 =?elem(X2 , c nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );..
