16. Управление вычислениями логических программ. Оператор отсечения (В.А. Захаров - Лекции)
Описание файла
Файл "16. Управление вычислениями логических программ. Оператор отсечения" внутри архива находится в папке "В.А. Захаров - Лекции". PDF-файл из архива "В.А. Захаров - Лекции", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 16.Управление вычислениямилогических программ.Оператор отсечения.УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИВопросы:А как организовано вычислениелогических программ накомпьютере?Как устроен интерпретаторлогических программ?УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПростейший способ организации работы логических программна основе стандартной стратегии обхода дереваSLD-резолютивных вычислений в глубину с возвратом — эторабота со стеком (или магазином ).В каждом элементе Sn стека содержится следующаяинформация:IТекущее целевое утверждение (запрос) Gn ;IКомпозиция всех ранее вычисленных унификаторовηn = (θ1 .
. . θn )|целев.перем ;IСчетчик использованных программных утвержденийcountn ;IСпециальные пометки (о некоторых из них будетрассказано далее).УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?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)УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?P(U, V ), R(U)Программа P:η = ε;P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;Протокол:SLD-резолюцияНОУ = {X1 /U, Y1 /V }(1)(2)(3)(4)count = 1?R(U), Q(V ), R(U)η = ε;count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:SLD-резолюцияНОУ = {U/b}count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Нет унификатораcount = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Нет унификатораcount = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Нет унификатораcount = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Унификацияcount = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)SLD-резолюцияη = {U/b, V /c}; count = 1НОУ = {V /c}УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Нет унификатораη = {U/b, V /c}; count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Нет унификатораη = {U/b, V /c}; count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Унификацияη = {U/b, V /c}; count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)SLD-резолюцияη = {U/b, V /c}; count = 3НОУ = εη = {U/b, V /c}УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Успех: η = {U/b, V /c}η = {U/b, V /c}; count = 3η = {U/b, V /c}УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Откатη = {U/b, V /c}; count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Нет унификатораη = {U/b, V /c}; count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Откатcount = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?P(U, V ), R(U)Программа P:η = ε;P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;Протокол:SLD-резолюцияНОУ = {U/X1 , V /X1 }(1)(2)(3)(4)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 1Протокол:SLD-резолюцияНОУ = {X1 /c}УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 1Протокол:Нет унификатораУПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 2Протокол:Нет унификатораУПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 3Протокол:Нет унификатораУПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 4Протокол:Нет унификатораУПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?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)УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИД.