Ещё одни лекции В.А. Захарова, страница 29
Описание файла
PDF-файл из архива "Ещё одни лекции В.А. Захарова", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 29 страницы из PDF
, Cn не имеетSLDNF-резольвент, и вычисление этого запроса являетсябесконечным («сингулярная бесконечность»).Условие существования бесконечного вычисления запросаnot(C0 ) описано не вполне строго, поскольку обнаружениеуспешного вычисления существенно зависит от стратегииобхода дерева SLD-резолютивных вычислений. Так, например,стандартная стратегия обхода в глубину может не обнаружитьсуществующего успешного вычисления (почему? ).ОПЕРАТОР notТеорема (корректности SLDNF-резолюции)Если запрос G : ? not(C0 ) к хорновской логической программеP имеет успешное SLDNF-резолютивное вычисление, тоP |=CWA ¬∃y C0 .ДоказательствоСамостоятельно .А вот обратное утверждение (теорема полноты) дляSLDNF-резолютивного вычисления будет уже неверно.ОПЕРАТОР notПример.Рассмотрим программу поиска всех тех букв X слова L ,которые не содержатся в слове L .P : S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ← ;E (X , Y L) ← E (X , L);..и обратимся к ней с запросом..
..G0 : ? S(X , a b nil, b c nil)...S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..?S(X , a b t nil, b c nil)(1)(2)(3)..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil)(1).. ..?t?E (X , a.b .nil),not(E (X , b .c .nil))θ1 = {X1 /X , L /aL /bbcnil,nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);..
..(1)(2)(3)?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil}(2)t..?not(E (a, b c nil))bcnil,nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L /aL /bbcnil,nil}..?E (a, b tc nil)..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil)..
.., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L /aL /bbcnil,nil}..?E (a, b tc nil)(3)?t.?E (a, c nil)..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L /aL /bbcnil,nil}..?E (a, b tc nil)(3)?t.?E (a, c nil)(3)?t?E (a, nil)..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L /aL /bbcnil,nil}..?E (a, b tc nil)(3)?t.?E (a, c nil)(3)?t?E (a, nil)failure..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil)..
.., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L /aL /bbcnil,nil}..?E (a, b tc nil)(3)?t.?E (a, c nil)(3)6?t?E (a, nil)failure..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil)..
.., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L /aL /bbcnil,nil}..?E (a, b tc nil)(3)6?t.?E (a, c nil)(3)6?t?E (a, nil)failure..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)Успех?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1nil}(2)t..?not(E (a, b c nil))/X , L /aL /bbcnil,nil}..?E (a, b tc nil)(3)6?t.?E (a, c nil)(3)6?t?E (a, nil)failure..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);..
..(1)(2)(3)?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil}(2)t..?not(E (a, b c nil))θ3 = ε?tОтвет: {X /a}bcnil,nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil}(2)t..?not(E (a, b c nil))θ3 = ε6?tОтвет: {X /a}bcnil,nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil)..
.., a.b .nil),. ?t?E (Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil}(2)t..?not(E (a, b c nil))θ3 = ε6?tОтвет: {X /a}bcnil,nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..(1)(2)(3)?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t@?E@(Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil,nil}nil}(2)t..(3) @ θ?not(E (a, b c nil))θ3 = εbc6?tОтвет: {X /a}4= {X2 /X , Y2 /a, L2 /bRt@....?E (X , b nil),not(E (X , b c nil))nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil).. .., a.b .nil),.
?t@?E@(Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil,nil}nil}(2)t..(3) @ θ?not(E (a, b c nil))θ3 = εbc6?tОтвет: {X /a}4= {X2 /X , Y2 /a, L2 /bRt@....?E (X , b nil),not(E (X , b c nil))(2)θ5 = {X /b, L3 /nil}?t..?not(E (b, b c nil))nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3)..
....?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t@?E@(Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1L /bbct..(3) @ θ?not(E (a, b c nil))6?tОтвет: {X /a}4= {X2 /X , Y2 /a, L2 /bRt@.?E (b, b tc nil)nil,nil}nil}(2)θ3 = ε/X , L /a...?E (X , b nil),not(E (X , b c nil))(2)θ5 = {X /b, L3 /nil}?t..?not(E (b, b c nil))nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ....?S(X , a b t nil, b c nil)..
.., a.b .nil),. ?t@?E@(Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1L /bbct..(3) @ θ?not(E (a, b c nil))6?tОтвет: {X /a}4= {X2 /X , Y2 /a, L2 /bRt@.?E (b, b tc nil)nil,nil}nil}(2)θ3 = ε/X , L /a..(2)?t.?E (X , b nil),not(E (X , b c nil))(2)θ5 = {X /b, L3 /nil}?t..?not(E (b, b c nil))nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..Неудача..?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t@?E@(Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1L /bbct..(3) @ θ?not(E (a, b c nil))6?tОтвет: {X /a}4= {X2 /X , Y2 /a, L2 /bRt@.?E (b, b tc nil)nil,nil}nil}(2)θ3 = ε/X , L /a..(2)?t.?E (X , b nil),not(E (X , b c nil))(2)θ5 = {X /b, L3 /nil}?t..?not(E (b, b c nil))nil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3)..
..?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t@?E@(Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil,nil}nil}(2)t..(3) @ θ?not(E (a, b c nil))θ3 = εbc6?tОтвет: {X /a}4= {X2 /X , Y2 /a, L2 /bRt@....?E (X , b nil),not(E (X , b c nil))(2)θ5 = {X /b, L3 /nil}?t..?not(E (b, b c nil))failurenil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil)..
.., a.b .nil),. ?t@?E@(Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil,nil}nil}(2)t..(3) @ θ?not(E (a, b c nil))θ3 = εbc6?tОтвет: {X /a}4= {X2 /X , Y2 /a, L2 /bRt@....?E (X , b nil),not(E (X , b c nil))(2)6θ5 = {X /b, L3 /nil}?t..?not(E (b, b c nil))failurenil}..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t@?E@(Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil,nil}nil}(2)t..(3) @ θ?not(E (a, b c nil))θ3 = εbc6?tОтвет: {X /a}4= {X2 /X , Y2 /a, L2 /bRt@..
.@.nil}?E (X , b nil),not(E (X , b c nil))(2)6θ5 = {X3 /X , Y3 /b, L3 /nil}(3) @θ5 = {X /b, L3 /nil}?t..?not(E (b, b c nil))failure@ ?E (X , nil),Rt@..not(E (X , b c nil))..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil).. .., a.b .nil),. ?t@?E@(Xnot(E(X , b .c .nil))(1)θ2 = {X /a, L1 /bθ1 = {X1 /X , L /aL /bnil,nil}nil}(2)t..(3) @ θ?not(E (a, b c nil))θ3 = εbc6?tОтвет: {X /a}4= {X2 /X , Y2 /a, L2 /bRt@.. .@.nil}?E (X , b nil),not(E (X , b c nil))(2)6θ5 = {X3 /X , Y3 /b, L3 /nil}(3) @θ5 = {X /b, L3 /nil}?t..?not(E (b, b c nil))failure@ ?E (X , nil),Rt@..not(E (X , b c nil))failure..S(X , L , L ) ← E (X , L ), not(E (X , L ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil).. .., a.b .nil),.