Ещё одни лекции В.А. Захарова, страница 20
Описание файла
PDF-файл из архива "Ещё одни лекции В.А. Захарова", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 20 страницы из PDF
.θ = НОУ(R(X , X nil), R(X1 nil, Y1 )) ={X /X1 nil, Y1 /(X1 nil) nil}.КОММЕНТАРИИ.Вычисляем Наиболее Общий Унификатор.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D = R(X1 nil, Y1 ) ←;... .θ = НОУ(R(X , X nil), R(X1 nil, Y1 )) ={X /X1 nil, Y1 /(X1 nil) nil}G = ()θ?.КОММЕНТАРИИ.Строим SLD-резольвентуSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D = R(X1 nil, Y1 ) ←;?G = ... .θ = НОУ(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 = R(X1 nil, X1 ) ←;КОММЕНТАРИИ.Переименовываем переменные в выбранном утверждении,SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D = R(X1 nil, X1 ) ←;..НОУ(R(X , X nil), R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Атомы неунифицируемы!SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D = R(X1 nil, X1 ) ←;..НОУ(R(X , X nil), R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Значит, SLD-резольвенту нельзя построить.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D = R(X1 nil, X1 ) ←;..НОУ(R(X , X nil), R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Нужно выделить другую подцель иливыбрать другое программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)ПустьG0 = ? C1 , C2 , .
. . , Cm — целевое утверждение,P = {D1 , D2 , . . . , DN } — хорновская логическая программа.Тогда (частичным) SLD-резолютивным вычислением ,порожденным запросом G0 к логической программе Pназывается последовательность троек (конечная илибесконечная)(Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . . , (Djn , θn , Gn ), . . . ,в которой для любого i, i ≥ 1,Dji ∈ P, θi ∈ Subst, Gi — целевое утверждение (запрос);запрос Gi является SLD-резольвентой программногоутверждения Dji и запроса Gi−1 с унификатором θi .SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)Частичное SLD-резолютивное вычислениеcomp = (Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), .
. . , (Djk , θn , Gn )называетсяуспешным вычислением (SLD-резолютивнымопровержением), если Gn = ;бесконечным вычислением , если comp — это бесконечнаяпоследовательность;тупиковым вычислением , если comp — это конечнаяпоследовательность, и при этом для выделенной подцелизапроса Gn невозможно построить ни однойSLD-резольвенты.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)ПустьG0 = ? C1 , C2 , .
. . , Cm — целевое утверждение с целевымипеременными Y1 , Y2 , . . . , Yk ,P = {D1 , D2 , . . . , DN } — хорновская логическая программа,comp = (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 :...? 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)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 );..
θ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)elem(X3 ,X3 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 );?.G2 =?elem(X2 , c nil)elem(X3 ,X3 nil);.θ3 = {X2 /c, X3 /c}?G3 = УСПЕХ!.θ2 = {X1 /X2 , Y2 /b, L2 /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 );?.θ2 = {X1 /X2 , Y2 /b, L2 /c nil}.G2 =?elem(X2 , c nil)elem(X3 ,X3 nil);.θ3 = {X2 /c, X3 /c}?G3 = УСПЕХ!Вычисленный ответ: θ = (θ1 θ2 θ3 )|X = {X /c}SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)..G0 =?elem(c, a b nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)...G0 =?elem(c, a b nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)...G0 =?elem(c, a b nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.
θ1 = {X1 /c, Y1 /a, L1 /b nil}?.G1 =?elem(c, b nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)...G0 =?elem(c, a b nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );. θ1 = {X1 /c, Y1 /a, L1 /b nil}?..G1 =?elem(c, b nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)...G0 =?elem(c, a b nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );. θ1 = {X1 /c, Y1 /a, L1 /b nil}?..G1 =?elem(c, b nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?θ2 = {X1 /X2 , Y2 /b, L2 /nil}G2 =?elem(c, nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)...G0 =?elem(c, a b nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.
θ1 = {X1 /c, Y1 /a, L1 /b nil}?..G1 =?elem(c, b nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?θ2 = {X1 /X2 , Y2 /b, L2 /nil}.G2 =?elem(c, nil)elem(X3 ,X3 L3 );Нет унификатораSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)...G0 =?elem(c, a b nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );. θ1 = {X1 /c, Y1 /a, L1 /b nil}?..G1 =?elem(c, b nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?θ2 = {X1 /X2 , Y2 /b, L2 /nil}.G2 =?elem(c, nil)elem(X3 ,Y3 L3 ) ← elem(X3 ,L3 );Нет унификатораSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)...G0 =?elem(c, a b nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.
θ1 = {X1 /c, Y1 /a, L1 /b nil}?..G1 =?elem(c, b nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?θ2 = {X1 /X2 , Y2 /b, L2 /nil}G2 =?elem(c, nil)failureНет SLD-резольвентыТУПИК!SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X )SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X )G0 =?elem(a, X )SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X ).G0 =?elem(a, X )elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X ).G0 =?elem(a, X )elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.
θ1 = {X1 /a, X /Y1 L1 }?G1 =?elem(a, L1 )SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X ).G0 =?elem(a, X )elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );. θ1 = {X1 /a, X /Y1 L1 }?.G1 =?elem(a, L1 )elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X ).G0 =?elem(a, X )elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );. θ1 = {X1 /a, X /Y1 L1 }?.G1 =?elem(a, L1 )elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?.θ2 = {X2 /a, L1 /Y2 L2 }G2 =?elem(a, L2 )SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X ).G0 =?elem(a, X )elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.
