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

. &ϕn ) → ϕ0 , или,что равносильно, противоречивости системы формулS = {ϕ1 , ϕ2 , . . . , ϕn , ¬ϕ0 }.Для проверки противоречивости системы S применяем методрезолюций.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯНо метод резолюций позволяет решать и более изощренныезадачи.Пусть имеется база знаний Γ = {ϕ1 , ϕ2 , . . . , ϕn } и запросQ = ϕ0 (x1 , . . .

, xm ).Задача: вычислить значения переменных x1 , . . . , xm , прикоторых запрос Q логически следует из базы знаний Γ.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯРешить эту задачу можно попытаться так:задачу проверки логического следствия{ϕ1 , ϕ2 , . . . , ϕn } |= ∃x1 . . . ∃xm ϕ0 (x1 , .

. . , xm ).свести к проверке противоречивости системы формулS = {ϕ1 , ϕ2 , . . . , ϕn , ¬ϕ0 (x1 , . . . , xm )}(здесь x1 , . . . , xm по умолчанию связаны квантором ∀),построить резолютивное опровержение S, иприменить последовательность унификаторовθ1 , θ2 , .

. . , θN , вычисленных по ходу построениярезолютивного вывода, к целевым переменным x1 , . . . , xm :x1 θ 1 θ 2 . . . θ N ,...,xm θ 1 θ 2 . . . θ N .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯЭтот трюк сработал при решении задачи о «любовномквадрате Саша–Даша–Паша–пиво».Попробуем применить его еще раз для решения какой-нибудьдругой вычислительной задачи.Поиск пути в графе.Пусть задан ориентированный граф Γ , в котором выделеныдве вершины u и v . Требуется найти маршрут из вершины u ввершину v .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.граф Γv3y @@v1yv2v4y-y@@6@@@R yv5@@R yv@6v7yРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.граф Γv3y @@v1yv2v4y-y@@6@@@R yv5@@R yv@6v7yРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.граф Γv3y @@v1yv2v4y-y@@6@@@R yv5@@R yv@6v7yРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Вначале нужно суметь сформулировать эту задачу на языкелогики предикатов.Граф Γ может быть задан перечнем его вершин и дуг.

Введемконстанты v1 , v2 , . . . , vn , . . . для обозначения вершинграфов;предикатный символ Vert (1) для обозначения свойства:«x — вершина графа» ;предикатный символ Arc (2) для обозначения свойства:«x, y — дуга графа».Чтобы отличать переменные от констант, в дальнейшемусловимся обозначать переменные ЗАГЛАВНЫМИБУКВАМИ, а константы — строчными буквами.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Тогда граф может быть описан следующим набором формуллогики предикатов.KBΓ =ϕ1 = Vert(v1 ), ψ1 = Arc(v1 , v2 ),ϕ2ϕ3ϕ4ϕ5ϕ6= Vert(v2 ),= Vert(v3 ),= Vert(v4 ),= Vert(v5 ),= Vert(v6 ),ϕ7 = Vert(v7 ),ψ2ψ3ψ4ψ5ψ6= Arc(v2 , v3 ),= Arc(v2 , v5 ),= Arc(v3 , v6 ),= Arc(v5 , v4 ),= Arc(v4 , v6 ), ψ7 = Arc(v6 , v5 )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Ориентированный путь в графе — это последовательность(список) дуг. Значит, нужно иметь подходящую структуруданных для представления списка на языке логики предикатов.Для этого мы введемспециальную константу nil для обозначения пустогосписка, не содержащего ни одного элемента;специальный функциональный символ (2) дляобозначения двухместной операции присоединенияэлемента x к списку y в качестве заголовка (конструкторсписков )..РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе..При помощи введенных символов nil и определимспециальное множество термов — списки :константа nil — это список;если t — произвольный терм, а T — список,то терм (t, T ) — это список;других списков нет..Терм t называтся заголовком , а T — хвостом списка..(t, T ).Чтобы сделать обозначения более естественными, мы будемзаписывать знак двухместной операции между аргументами(инфиксная запись), как это делается для операций +, ×.Таким образом, запись.(t , t ) равносильна записи t .t .1212РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Примеры списковПустой список:nilCписок из одного элемента X :.X nil.

.Последовательность букв а,б,в,г: а.(б.(в.(г.nil)))Упорядоченная пара X , Y :Таблица (матрица)1 23 4X (Y nil):. . . (3.(4.nil)).nil(1 (2 nil))РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Поскольку в большинстве случаев списки используются дляпредставления конечных последовательностей, упростимзапись линейных списков:условимся опускать скобки, считая по умолчанию, что всескобки ассоциируются вправо, т.е. запись....а (б (в (г nil)))будет считаться равносильной записи....а б в г nilРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе..Терм а.б.в.г вообще не является списком (почему? );Терм (1.nil).2.nil.nil обозначает список, состоящий из трехЕще несколько примеров списковТерм nil nil обозначает список, состоящий из одного элемента— пустого списка;элементов:первый элемент — это список, состоящий из одного элемента 1,второй элемент — это константа 2,третий элемент — пустой список..Следует помнить, что термы X nil и X — существенноразличные (имеют разные типы):X nil — это список (массив) из одного элемента X ,X — это просто элемент (переменная или константа)..РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Таким образом, маршрут в ориентированном графе — этосписок дуг, в котором каждая дуга — это список, состоящий издвух вершин...

. .. .Пример: (v1 v2 nil) (v2 v3 nil) nil — это маршрут,состоящий из двух дуг v1 , v2 и v2 , v3 .А теперь запишем на языке логики предикатов определениемаршрута в ориентированном графе. Для этого введемтрехместный предикатный символ R (3) :R(X , Y , t) будет обозначать утверждение о том, что терм tзадает маршрут из вершины X в вершину Y .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Определение маршрута в графе состоит из двух частей:χ1 = ∀X R(X , X , nil)«из X в X ведет пустой маршрут»;.. .χ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 = X , Y , 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 |= ∃X Q(X )Cведем вопрос о логическом следствии к вопросу опротиворечивости формулы 77ϕi &ψj & χ1 & χ2 → ∃X Q(X )¬i=1j=1Далее приводим полученную формулу к ПНФ, к ССФ, иизвлекаем систему дизъюнктов S.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Построим резолютивное опровержение полученной системыдизъюнктов S:S=ϕ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 ) ∨ ¬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),РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Φ0 = ¬R(v1 ,v6 ,X )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе... .χ2 = ¬Arc(X1 ,Y1 )∨¬R(Y1 ,Z1 ,U1 )∨R(X1 ,Z1 ,(X1 Y1 nil) U1 )Φ0 = ¬R(v1 ,v6 ,X )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе... .¬Arc(X1 ,Y1 )∨¬R(Y1 ,Z1 ,U1 )∨R(X1 ,Z1 ,(X1 Y1 nil) U1 )θ1 = {X /(v1 Y1 nil) U1 , X1 /v1 , Z1 /v6 }Φ0 = ¬R(v1 ,v6 ,X )D1= ¬Arc(v1 ,Y1 )∨¬R(Y1 ,v6 ,U1 ).. .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе...

.χ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 = ¬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 }D2 = ¬R(v2 ,v6 ,U1 )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе...

.χ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 )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе... .χ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..