LectLog11 (1158003), страница 2
Текст из файла (страница 2)
.χ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 = ¬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 }D20 = ¬R(v2 ,v6 ,U1 )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе... .χ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 )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе... .χ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 )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе... .χ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 )D30 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )D30 = ¬Arc(v2 ,Y2 )∨¬R(Y2 ,v6 ,U2 )ψ2 = Arc(v2 , v3 )D40 = ¬R(v3 ,v6 ,U2 )θ4 = {Y2 /v3 }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 )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 )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 )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 )D60 = ¬R(v6 , v6 , U3 )θ6 = {Y3 /v6 }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 )χ1 = R(X4 , X4 , nil)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 )χ1 = R(X4 , X4 , nil)θ7 = {X4 /v6 , U3 /nil}D70 = 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 )χ1 = R(X4 , X4 , nil)θ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 θ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РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.граф Γv1yv3v2-y@@y @@@v4y6@R yv@6v7y@@@R yv5.
. . .. . .. .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 )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?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 (кино)D2 = R ∨ E (парк)@@@θ1 = {X /кино}@@@R @θ2 = {X /парк}@@R @D3 = ¬RD4 = RQQQQθ3 = εQQQsQ+РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?D0 = ¬E (X )@@D1 = ¬R ∨ E (кино)D2 = R ∨ E (парк)@@@θ1 = {X /кино}@@@R @θ2 = {X /парк}@@R @D3 = ¬RD4 = RQQQQθ3 = εQQQsQ+Резолютивное опровержение построеноРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯГде мы проведем вечер?Построив резолютивное опровержение, мы можем бытьуверены, что{ϕ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..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
