11. Стратегии резолютивного вывода. Вычислительные возможности метода резолюций (В.А. Захаров - Лекции), страница 2

.χ2 = ∀X ∀Y ∀Z ∀U (Arc(X , Y )&R(Y , Z , U) → R(X , Z , (X Y nil) U))«если из X в Y ведет дуга, а из Y в Z ведет маршрут U,то из X в Z ведет маршрут t 0 = hX , Y i, U».РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Итак, мы имеемБазу знаний KB, состоящую из формулϕi , 1 ≤ i ≤ 7,ψi , 1 ≤ i ≤ 7,χ1 , χ2 ,при помощи которых определяется устройство графа Γ изнания о том, что такое маршрут в графе.Запрос к базе знаний Q(X ) = R(v1 , v6 , X ) с одной целевойпеременной X .Наша задача: найти такое значение t целевой переменной X ,при котором имеет место логическое следствиеKB |= Q(t).РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Будем решать задачу поиска пути методом резолюций.KB |= ∃XQ(X )Cведем вопрос о логическом следствии к вопросу опротиворечивости формулы ^77^ϕi &¬ψj & χ1 & χ2 → ∃X Q(X )i=1j=1Далее приводим полученную формулу к ПНФ, к ССФ, иизвлекаем систему дизъюнктов S.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Построим резолютивное опровержение полученной системыдизъюнктов S:nS=ϕ1 = Vert(v1 ),ψ1 = Arc(v1 , v2 ),ϕ2 = Vert(v2 ),ϕ3 = Vert(v3 ),ϕ4 = Vert(v4 ),ϕ5 = Vert(v5 ),ϕ6 = Vert(v6 ),ϕ7 = Vert(v7 ),χ1 = R(X , X , nil),χ2 = ¬Arc(X , Y ) ∨o¬R(Y , Z , U)Φ0 = ¬R(v1 , v6 , X )ψ2ψ3ψ4ψ5ψ6ψ7= Arc(v2 , v3 ),= Arc(v2 , v5 ),= Arc(v3 , v6 ),= Arc(v5 , v4 ),= Arc(v4 , v6 ),= Arc(v6 , v5 ),..

.∨ R(X , Z , (X Y nil) U),РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе... .χ2 = ¬Arc(X1 ,Y1 )∨¬R(Y1 ,Z,U )∨R(X1 ,Z1 ,(X1 Y1 nil) U1 )1 1Φ0 = ¬R(v1 ,v6 ,X )θ1 = {X /(v1 Y1 nil) U1 , X1 /v1 , Z1 /v6 }.. .D10 = ¬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 )D20 = ¬R(v2 ,v6 ,U1 )..

.θ3 = {U1 /(v2 Y2 nil) U2 , X2 /v2 , Z2 /v6 }D30 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )D30 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )θ4 = {Y2 /v3 } ¬Arc(X3 ,Y3 )∨¬R(Y3 ,Z3 ,U3 )∨R(X3 ,Z3 ,(X3 Y3 nil) U3 )D40 = ¬R(v3 ,v6 ,U2 )θ5 = {U2 /(v3 Y3 nil) U3 , X3 /v3 , Z3 /v6 }.. ... .D50 = ¬Arc(v3 ,Y3 )∨¬R(Y3 ,v6 ,U3 )ψ4 = Arc(v3 , v6 )θ6 = {Y3 /v6 }D60 = ¬R(v6 , v6 , U3 )χ = R(X , X , nil)144θ7 = {X4 /v6 , U3 /nil}D70 = Вывод успешно завершен.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Итак, система дизъюнктов 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 θ7 = (v1 v2 nil) (v2 v3 nil) (v3 v6 nil) nilРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.граф Γv1yv3v2-y@@y @@@v4y6@R yv@6v7y@@@Ryv5.

. . .. . .. .X θ1 θ2 θ3 θ4 θ5 θ6 θ7 = (v1 v2 nil) (v2 v3 nil) (v3 v6 nil) nilРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯНам опять повезло, и метод резолюций вычислил правильныйответ.Неужели так хорошо и красиво бывает всегда?Рассмотрим еще одну задачу.Где мы проведем вечер?Если вечером будет идти дождь, то мы пойдем в кино, а еслидождя не будет, то мы пойдем в парк. Где же мы проведемвечер?РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?Введем необходимые константы и предикаты:Iкино и парк — константы;IR (0) — 0-местный предикатный символ, обозначающийутверждение «вечером пойдет дождь»;IE (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 )@@D1 = ¬R ∨ E (кино)D2 = R ∨ E (парк)@@@θ1 = {X /кино}@@@R @θ2 = {X /парк}@@R @D3 = ¬RD4 = RQQQQθ3 = εQQQQs+Резолютивное опровержение построеноРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?Построив резолютивное опровержение, мы можем бытьуверены, что{ϕ1 , ϕ2 } |= ∃X E (X ),т.е. куда-то вечером мы пойдем.Но куда же мы пойдем?Поскольку в этом выводе вместо целевой переменной X былиодновременно (параллельно) подставлены разные термы кинои парк, то все, что мы можем сказать — это X ∈ {кино, парк}.Мы сумели доказать существование требуемого предмета X , ноне сумели вычислить его конкретное значение.

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

Удалось обнаружить широкий классформул, для которых резолютивное опровержение всегда имеетлинейную структуру. Это — хорновские дизъюнкты .ОпределениеЛитера L называется положительной , если L — это атом.Литера L называется отрицательной , если L = ¬A, где A — этоатом.Дизъюнкт D = L1 ∨ L2 ∨ · · · ∨ Ln называется хорновскимдизъюнктом (horn clause ), если среди литер L1 , L2 , . . . , Lnимеется не более одной положительной литеры.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПримеры.Хорновские дизъюнкты:D10D20D30D40====¬L(Паша, Y ) ∨ ¬L(X , Y ) ∨ L(Паша, X ),¬Arc(v1 , Y1 ) ∨ ¬R(Y1 , v6 , U1 ),Arc(v6 , v4 ),¬R ∨ E (кино).А вот этот дизъюнкт — нехорновский:D 00 = 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..