Ещё одни лекции В.А. Захарова, страница 17

.= ¬Arc(v1 ,Y1 )∨¬R(Y1 ,v6 ,U1 )ψ1 = Arc(v1 , v2 )θ2 = {Y1 /v2 }.. . ¬Arc(X2 ,Y2 )∨¬R(Y2 ,Z2 ,U2 )∨R(X2 ,Z2 ,(X2 Y2 nil) U2 )D2 = ¬R(v2 ,v6 ,U1 )θ3 = {U1 /(v2 Y2 nil) U2 , X2 /v2 , Z2 /v6 }.. .D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе... .χ2 = ¬Arc(X1 ,Y1 )∨¬R(Y1 ,Z,U )∨R(X1 ,Z1 ,(X1 Y1 nil) U1 )1 1θ1 = {X /(v1 Y1 nil) U1 , X1 /v1 , Z1 /v6 }Φ0 = ¬R(v1 ,v6 ,X )D1.. .= ¬Arc(v1 ,Y1 )∨¬R(Y1 ,v6 ,U1 )ψ1 = Arc(v1 , v2 )θ2 = {Y1 /v2 }.. .

¬Arc(X2 ,Y2 )∨¬R(Y2 ,Z2 ,U2 )∨R(X2 ,Z2 ,(X2 Y2 nil) U2 )D2 = ¬R(v2 ,v6 ,U1 )θ3 = {U1 /(v2 Y2 nil) U2 , X2 /v2 , Z2 /v6 }.. .D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )θ4 = {Y2 /v3 }D4 = ¬R(v3 ,v6 ,U2 )D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )θ4 = {Y2 /v3 }¬Arc(X,Y)∨¬R(Y,Z3 33 3 ,U3 )∨R(X3 ,Z3 ,(X3 Y3 nil) U3 )D4 = ¬R(v3 ,v6 ,U2 ).. .D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )θ4 = {Y2 /v3 }¬Arc(X,Y)∨¬R(Y,Z3 33 3 ,U3 )∨R(X3 ,Z3 ,(X3 Y3 nil) U3 )D4 = ¬R(v3 ,v6 ,U2 )θ5 = {U2 /(v3 Y3 nil) U3 , X3 /v3 , Z3 /v6 }.. ...

.D5 = ¬Arc(v3 ,Y3 )∨¬R(Y3 ,v6 ,U3 )D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )θ4 = {Y2 /v3 }¬Arc(X,Y)∨¬R(Y,Z3 33 3 ,U3 )∨R(X3 ,Z3 ,(X3 Y3 nil) U3 )D4 = ¬R(v3 ,v6 ,U2 )θ5 = {U2 /(v3 Y3 nil) U3 , X3 /v3 , Z3 /v6 }.. ... .D5 = ¬Arc(v3 ,Y3 )∨¬R(Y3 ,v6 ,U3 )ψ4 = Arc(v3 , v6 )D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )θ4 = {Y2 /v3 }¬Arc(X,Y)∨¬R(Y,Z3 33 3 ,U3 )∨R(X3 ,Z3 ,(X3 Y3 nil) U3 )D4 = ¬R(v3 ,v6 ,U2 )θ5 = {U2 /(v3 Y3 nil) U3 , X3 /v3 , Z3 /v6 }..

... .D5 = ¬Arc(v3 ,Y3 )∨¬R(Y3 ,v6 ,U3 ) ψ4 = Arc(v3 , v6 )D6 = ¬R(v6 , v6 , U3 )θ6 = {Y3 /v6 }D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )θ4 = {Y2 /v3 }¬Arc(X,Y)∨¬R(Y,Z3 33 3 ,U3 )∨R(X3 ,Z3 ,(X3 Y3 nil) U3 )D4 = ¬R(v3 ,v6 ,U2 )θ5 = {U2 /(v3 Y3 nil) U3 , X3 /v3 , Z3 /v6 }.. ... .D5 = ¬Arc(v3 ,Y3 )∨¬R(Y3 ,v6 ,U3 )ψ4 = Arc(v3 , v6 )θ6 = {Y3 /v6 }D6 = ¬R(v6 , v6 , U3 )χ1 = R(X4 , X4 , nil)D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )θ4 = {Y2 /v3 }¬Arc(X,Y)∨¬R(Y,Z3 33 3 ,U3 )∨R(X3 ,Z3 ,(X3 Y3 nil) U3 )D4 = ¬R(v3 ,v6 ,U2 )θ5 = {U2 /(v3 Y3 nil) U3 , X3 /v3 , Z3 /v6 }.. ... .D5 = ¬Arc(v3 ,Y3 )∨¬R(Y3 ,v6 ,U3 )ψ4 = Arc(v3 , v6 )θ6 = {Y3 /v6 }D6 = ¬R(v6 , v6 , U3 )D7 = χ1 = R(X4 , X4 , nil)θ7 = {X4 /v6 , U3 /nil}D3 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )θ4 = {Y2 /v3 }¬Arc(X,Y)∨¬R(Y,Z3 33 3 ,U3 )∨R(X3 ,Z3 ,(X3 Y3 nil) U3 )D4 = ¬R(v3 ,v6 ,U2 )θ5 = {U2 /(v3 Y3 nil) U3 , X3 /v3 , Z3 /v6 }..

... .D5 = ¬Arc(v3 ,Y3 )∨¬R(Y3 ,v6 ,U3 )ψ4 = Arc(v3 , v6 )θ6 = {Y3 /v6 }D6 = ¬R(v6 , v6 , U3 )χ1 = R(X4 , X4 , nil)θ7 = {X4 /v6 , U3 /nil}D7 = Вывод успешно завершен.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Итак, система дизъюнктов S противоречива, т.

е. маршрут извершины v1 в вершину v6 существует. Но каков этот маршрут?Рассмотрим последовательность вычисленных унификаторовθ1θ2θ3θ4θ5θ6θ7=======.. ... ... .{X /(v1 Y1 nil) U1 , X1 /v1 , Z1 /v6 }{Y1 /v2 }{U1 /(v2 Y2 nil) U2 , X2 /v2 , Z2 /v6 }{Y2 /v3 }{U2 /(v3 Y3 nil) U3 , X3 /v3 , Z3 /v6 }{Y3 /v6 }{X4 /v6 , U3 /nil}и применим их к целевой переменной X :X θ1 θ2 θ3 θ4 θ5 θ6 θ6 θ7 =???РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Итак, система дизъюнктов S противоречива, т. е.

маршрут извершины v1 в вершину v6 существует. Но каков этот маршрут?Рассмотрим последовательность вычисленных унификаторовθ1θ2θ3θ4θ5θ6θ7=======.. ... ... .{X /(v1 Y1 nil) U1 , X1 /v1 , Z1 /v6 }{Y1 /v2 }{U1 /(v2 Y2 nil) U2 , X2 /v2 , Z2 /v6 }{Y2 /v3 }{U2 /(v3 Y3 nil) U3 , X3 /v3 , Z3 /v6 }{Y3 /v6 }{X4 /v6 , U3 /nil}и применим их к целевой переменной X :. . . .. . .. .(v1 v2 nil) (v2 v3 nil) (v3 v6 nil) nilРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.граф Γv3y @@v1yv2v4y-y@@@@R yv@6v7y6@@@R yv5.

. . .. . .. .X θ1 θ2 θ3 θ4 θ5 θ6 θ7 = (v1 v2 nil) (v2 v3 nil) (v3 v6 nil) nilРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯНам опять повезло, и метод резолюций вычислил правильныйответ.Неужели так хорошо и красиво бывает всегда?Рассмотрим еще одну задачу.Где мы проведем вечер?Если вечером будет идти дождь, то мы пойдем в кино, а еслидождя не будет, то мы пойдем в парк.

Где же мы проведемвечер?РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?Введем необходимые константы и предикаты:кино и парк — константы;R (0) — 0-местный предикатный символ, обозначающийутверждение «вечером пойдет дождь»;E (1) — 1-местный предикатный символ; E (X ) обозначаетутверждение «этим вечером наше развлечение — X ».База знаний:ϕ1 = R → E (кино),ϕ2 = ¬R → E (парк),Запрос: Q(X ) = E (X ).РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?1.

{ϕ1 , ϕ2 } |= ∃X E (X )?2. |= ϕ1 &ϕ2 → ∃X E (X )?3. Противоречива ли ¬ ϕ1 &ϕ2 → ∃X E (X ) ?3. Противоречива ли системаS = { D1 = ¬R ∨ E (кино),D2 = R ∨ E (парк),D0 = ¬E (X )}РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?D0 = ¬E (X )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?D0 = ¬E (X )D1 = ¬R ∨ E (кино)D2 = R ∨ E (парк)РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?D0 = ¬E (X )D1 = ¬R ∨ E (кино)@@θ1 = {X /кино}@@R @D3 = ¬R@@D2 = R ∨ E (парк)@@θ2 = {X /парк}@@R @D4 = RРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?D0 = ¬E (X )@@D1 = ¬R ∨ E (кино)@@θ1 = {X /кино}@@R @D2 = R ∨ E (парк)@@θ2 = {X /парк}@@R @D3 = ¬RD4 = RQQQQQθ3 = εQQsQ+РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?D0 = ¬E (X )@@D1 = ¬R ∨ E (кино)@@θ1 = {X /кино}@@R @D2 = R ∨ E (парк)@@θ2 = {X /парк}@@R @D3 = ¬RD4 = RQQQQQθ3 = εQQsQ+Резолютивное опровержение построеноРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?Построив резолютивное опровержение, мы можем бытьуверены, что{ϕ1 , ϕ2 } |= ∃X E (X ),т.

е. куда-то вечером мы пойдем.Но куда же мы пойдем?Поскольку в этом выводе вместо целевой переменной X былиодновременно (параллельно) подставлены разные термы кинои парк, то все, что мы можем сказать — это X ∈ {кино, парк}.Мы сумели доказать существование требуемого предмета X , ноне сумели вычислить его конкретное значение. Такиедоказательства называются неконструктивными .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯЧтобы резолютивный вывод позволял проводить вычисления,он должен быть конструктивным .Но, как показывает пример «вечернего развлечения», не всепротиворечивые системы дизъюнктов допускаютконструктивное резолютивное опровержение. Значит, длявычислительных целей нужно выбрать такой подкласс формуллогики предикатов, для которых резолютивное опровержениеоказывается конструктивным.Заметим, что при решении задач «любовного квадрата» и«маршрута в графе» мы построили линейное резолютивноеопровержение, а при решении задачи «вечернего развлечения»линейное резолютивное опровержение построить в принципеневозможно.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯЗначит, для того, чтобы использовать метод резолюций каксредство вычислений, нужно ограничиться линейнымрезолютивным выводом.

Удалось обнаружить широкий классформул, для которых резолютивное опровержение всегда имеетлинейную структуру. Это — хорновские дизъюнкты .ОпределениеЛитера L называется положительной , если L — это атом.Литера L называется отрицательной , если L = ¬A, где A — этоатом.Дизъюнкт D = L1 ∨ L2 ∨ · · · ∨ Ln называется хорновскимдизъюнктом (horn clause ), если среди литер L1 , L2 , . . .

, Lnимеется не более одной положительной литеры.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПримеры.Хорновские дизъюнкты:D1D2D3D4====¬L(Паша, Y ) ∨ ¬L(X , Y ) ∨ L(Паша, X ),¬Arc(v1 , Y1 ) ∨ ¬R(Y1 , v6 , U1 ),Arc(v6 , v4 ),¬R ∨ E (кино).А вот этот дизъюнкт — нехорновский:D = R ∨ E (парк).РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯХорновский дизъюнктA0 ∨ ¬A1 ∨ ¬A2 ∨ · · · ∨ ¬Anравносилен формулеA1 &A2 & .

. . &An → A0 ,которая выражает утверждение:«Если выполнены условия A1 и A2 и . . . и An , то верно A0 ».В подавляющем большинстве случаев именно в такой формемы выражаем наши позитивные знания (условные ибезусловные).РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯХорновский дизъюнкт¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cmравносилен формуле¬(C1 & C2 & . .

. & Cm ),и это есть отрицание запроса Q(X1 , . . . , Xk ) = C1 &C2 & . . . &Cm ,который выражает требование:«Найти такие значения переменных X1 , . . . , Xk , которыеудовлетворяют условиям C1 и C2 и . . . и Cm ».Большинство наших вопросов представлено именно в такойформе.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯРезолютивное опровержение систем хорновскихдизъюнктов — это вычисление ответов на простыезапросы, обращенные к базе позитивных знаний.Базы позитивных знаний (хорновские дизъюнкты)становятся, таким образом,ЛОГИЧЕСКИМИ ПРОГРАММАМИ .КОНЕЦ ЛЕКЦИИ 11.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 12.Хорновские логическиепрограммы: синтаксис.Декларативная семантикалогических программ.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПАРАДИГМЫ ПРОГРАММИРОВАНИЯИмперативное программирование : программа — это описаниепоследовательности операторов (команд).Языки: Assembler, Pascal, C, Java.Функциональное программирование : программа — это системауравнений, описывающая вычисляемую функцию.Языки: Lisp, ML, Haskel, Hope.Логическое программирование : программа — это множествоформул, описывающих условия решаемой задачи.Языки: Prolog, Datalog, Godel.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫСинтаксис логических программПусть σ = Const, Func, Pred — некоторая сигнатура, вкоторой определяются термы и атомы.«заголовок» ::= «атом»«тело» ::= «атом» | «тело», «атом»«правило» ::= «заголовок» ← «тело»;«факт» ::= «заголовок»;«утверждение» ::= «правило» | «факт»«программа» ::= «пусто» | «утверждение» «программа»«запрос» ::= | ? «тело»ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПримерыПравило: L(паша, Y ) ← L(Y , X ), L(паша, X );заголовоктелоФакт: L(даша, саша);Запрос (целевое утверждение ):? Умный(X ), Добрый(X ), Красивый(X ), Любит(X , меня) подцельподцельЗдесь X — целевая переменная .подцельподцельХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫТерминологияПусть P — логическая программа, D — программноеутверждение, а θ — подстановка.

ТогдаDθ — пример программного утверждения D,если θ — переименование, то Dθ — вариант программногоутверждения D,если VarDθ = ∅, то Dθ — основной пример программногоутверждения D,[D] — множество всех основных примеров программногоутверждения D,[P] — множество всех основных примеров всехутверждений программы P.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫТерминологияПусть G =?C1 , C2 , . . . , Cm — запрос. Тогдаатомы C1 , C2 , .