Лекции В.А. Захарова (1157993), страница 19

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 19)

. . , CmD 0 = A00 ← A01 , A02 , . . . , A0n ;θ = НОУ(Ci , A00 )КОММЕНТАРИИ.Вычисляем Наиболее Общий Унификатор.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , . . . , CmD 0 = A00 ← A01 , A02 , . . . , A0n ;θ = НОУ(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 ;θ = НОУ(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 );θ = НОУ(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 );θ = НОУ(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 ) ←;... .θ = НОУ(R(X , X nil), R(X1 nil, Y1 )) ={X /X1 nil, Y1 /(X1 nil) nil}0G = ()θ?.КОММЕНТАРИИ.Строим SLD-резольвенту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}.?G0 = КОММЕНТАРИИ.Вот она.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, X1 ) ←;..НОУ(R(X , X nil), R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Атомы неунифицируемы!SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, X1 ) ←;..НОУ(R(X , X nil), R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Значит, SLD-резольвенту нельзя построить.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, X1 ) ←;..НОУ(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 );..

θ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 );..

Характеристики

Список файлов лекций