LectLog11 (Старые лекции, в целом тоже самое)

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 11.Стратегии резолютивного вывода.Резолютивный вывод каксредство вычисления.СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАМетод резолюций не предписывает заранее никакогофиксированного порядка применения правил резолюции исклейки для вывода пустого дизъюнкта из противоречивогомножества дизъюнктов.Существуют различные стратегии резолютивного вывода ,налагающие дополнительные ограничения на выборподходящих пар дизъюнктов для получения резольвент.Стратегия резолютивного вывода называется полной , если онапозволяет вывести пустой дизъюнкт из любогопротиворечивого множества дизъюнктов.Рассмотрим пример.СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАПример.ПустьS= { D1D2D3D4= ¬P ∨ ¬Q ∨ R;= P ∨ R;= Q ∨ R;= ¬R}Можно построить много разных резольвент:D1 + D2 = ¬Q ∨ R, D1 + D3 = ¬P ∨ R, D1 + D4 = ¬P ∨ ¬Q,D2 + D4 = P, D3 + D4 = Q, и т.

д.Но как ограничиться только теми, которые действительнонужны для вывода ?СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАСемантическая резолюцияРазделим дизъюнкты на два подмножества по следующемупринципу:выберем H-интерпретацию I и положимS1I = {D : D ∈ S, I |= D},S2I = {D : D ∈ S, I 6|= D}.Наложим ограничение на применение правила резолюции:При построении резольвенты, оба дизъюнкта-предпосылкидолжны принадлежать разным множествам S1 и S2 .D1 = D10 ∨ L1 , D2 = D20 ∨ ¬L2, D1 ∈ S1I , D2 ∈ S2I , θ ∈ НОУ(L1 , L2 ).D0 = (D10 ∨ D20 )θТакое правило будем называть правилом I -резолюции .СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАПример.Пусть I = ∅, т.

е. I 6|= P, I 6|= Q, I 6|= R. ТогдаS1I : D1 = ¬P ∨ ¬Q ∨ R;D4 = ¬R;S2I : D2 = P ∨ R;D3 = Q ∨ R;I -резольвенты будут строиться так:S1 : D1 + D2 = ¬Q ∨ R; S2 : D4 + D2 = P;D1 + D3 = ¬P ∨ R;D4 + D3 = Q;(D1 + D2 ) + D3 = R;((D1 + D2 ) + D3 ) + D4 = СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАТеорема полноты I -резолюцииЕсли система дизъюнктов S противоречива, то для любойинтерпретации I существует успешный I -резолютивный выводпустого дизъюнкта из S.Доказательство:Самостоятельно.СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАЛинейная резолюцияПредположим, что в системе дизъюнктов S выделен некоторыйдизъюнкт D0 .Тогда резолютивный вывод пустого дизъюнкта из системыдизъюнктов S можно строить, руководствуясь следующимисоглашениями:IДля построения первой резольвенты D1 выбираетсядизъюнкт D0 и некоторый дизъюнкт D ∈ S \ {D0 };IДля построения i-ой резольвенты Di выбираетсярезольвента Di−1 , построенная на предыдущем шагевывода, и дизъюнкт D ∈ S.Резолютивный вывод такого вида будем называть линейнымрезолютивным выводом , инициированным дизъюнктом D0 .СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАПример.ПустьS= { D1 = ¬P ∨ ¬Q ∨ R; D2 = P ∨ R;D3 = Q ∨ R;D4 = ¬R}и выделенный дизъюнкт D0 — это D4 = ¬R.Тогда линейный резолютивный вывод будет таким:1.

D4 + D1 = ¬P ∨ ¬Q;2. (D4 + D1 ) + D2 = R ∨ ¬Q;3. ((D4 + D1 ) + D2 ) + D3 = R;4. (((D4 + D1 ) + D2 ) + D3 ) + D4 = .СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДАТеорема полноты линейного резолютивноговыводаЕсли система дизъюнктов S противоречива, а системадизъюнктов S 0 = S \ {D0 } непротиворечива, то существуетуспешный линейный резолютивный вывод пустого дизъюнкта из S.Доказательство:Самостоятельно.СТРАТЕГИИ РЕЗОЛЮТИВНОГО ВЫВОДААвтоматические пруверыfor1stThe World ChampionshipOrder Automated Theorem ProvingVampire (Manchester, A.

Voronkov),SPASS (Max Plank Institute, M. Keil),SNARK (AIC, California, E. Stikel),Otter (Argonne National Laboratory, USA, W. McCune),Gandalf (Goteborg, Tartu, T. Tammet),Carine (Montreal, Quebec, P. Haraoun).РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯМетод резолюций можно использовать для решения разныхзадач.

Например, для получения ответа на вопросА будет ли утверждение ϕ0 обязательно верно,если известно, что верны утверждения ϕ1 , ϕ2 , . . . , ϕn ?Здесь ϕ1 , ϕ2 , . . . , ϕn — это база знаний , ϕ0 — это запрос .РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯМатематическая постановка задачи такова: проверить{ϕ1 , ϕ2 , . . . , ϕn } |= ϕ0 .Проверка логического следствия сводится к проверкеобщезначимости: |= (ϕ1 &ϕ2 & . . . &ϕn ) → ϕ0 .Проверка общезначимости сводитсяк проверкепротиворечивости формулы ¬ (ϕ1 &ϕ2 & . . . &ϕ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 @@v1yv2v4-y@@y6@@@R yv5@@R yv@6v7yРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.граф Γv3y @@v1yv2v4-y@@y6@@@R yv5@@R yv@6v7yРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.граф Γv1yv3v2-y@@y @@@v4y6@@@R yv5@R yv@6v7yРЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Вначале нужно суметь сформулировать эту задачу на языкелогики предикатов.Граф Γ может быть задан перечнем его вершин и дуг.

ВведемIконстанты v1 , v2 , . . . , vn , . . . для обозначения вершинграфов;Iпредикатный символ Vert (1) для обозначения свойства:«x — вершина графа» ;Iпредикатный символ Arc (2) для обозначения свойства:«hx, y i — дуга графа».Чтобы отличать переменные от констант, в дальнейшемусловимся обозначать переменные ЗАГЛАВНЫМИБУКВАМИ, а константы — строчными буквами.РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Тогда граф может быть описан следующим набором формуллогики предикатов.KBΓ =nϕ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 ), oψ7 = Arc(v6 , v5 )РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Ориентированный путь в графе — это последовательность(список) дуг.

Значит, нужно иметь подходящую структуруданных для представления списка на языке логики предикатов.Для этого мы введемIспециальную константу nil для обозначения пустогосписка, не содержащего ни одного элемента;Iспециальный функциональный символ (2) дляобозначения двухместной операции присоединенияэлемента x к списку y в качестве заголовка (конструкторсписков )..РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе..При помощи введенных символов nil и определимспециальное множество термов — списки :Iконстанта nil — это список;Iесли t — произвольный терм, а T — список,то терм (t, T ) — это список;Iдругих списков нет..Терм t называтся заголовком , а T — хвостом списка.(t, T ).Чтобы сделать обозначения более естественными, мы будемзаписывать знак двухместной операции между аргументами(инфиксная запись), как это делается для операций +, ×..Таким образом, запись.(t , t ) равносильна записи t .t .1212РЕЗОЛЮТИВНЫЙ ВЫВОД КАК СРЕДСТВОВЫЧИСЛЕНИЯПоиск пути в графе.Примеры списковПустой список:nilCписок из одного элемента X :.X nil.

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

. .. .Пример: (v1 v2 nil) (v2 v3 nil) nil — это маршрут,состоящий из двух дуг hv1 , v2 i и hv2 , v3 i.А теперь запишем на языке логики предикатов определениемаршрута в ориентированном графе. Для этого введемтрехместный предикатный символ 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 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 |= ∃X Q(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 ) ∨ ¬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 ),..

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