Лекции 2-11. Математическая логика (до колка) (1161869), страница 16
Текст из файла (страница 16)
. . , 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 @@v1yv4v2y6-y@@@@@Ryv5@@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 ),ψ2ψ3ψ4ψ5ψ6= Arc(v2 , v3 ),= Arc(v2 , v5 ),= Arc(v3 , v6 ),= Arc(v5 , v4 ),= Arc(v4 , v6 ), oϕ7 = Vert(v7 ), ψ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 |= ∃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 ),т.е.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
