Лекции В.А. Захарова, страница 17

.Последовательность букв а,б,в,г: а.(б.(в.(г.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 ),т.е.

куда-то вечером мы пойдем.Но куда же мы пойдем?Поскольку в этом выводе вместо целевой переменной 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.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 12.Хорновские логическиепрограммы: синтаксис.Декларативная семантикалогических программ.Операционная семантикалогических программ:SLD–резолютивные вычисления.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПАРАДИГМЫ ПРОГРАММИРОВАНИЯИмперативное программирование : программа — это автомат,описывающий последовательности операторов (команд).Математическая модель: машины Тьюринга–Поста.Языки: Assembler, Pascal, C, Java.Функциональное программирование : программа — это системауравнений, описывающая вычисляемую функцию.Математическая модель: λ-исчисление Черча–Клини,уравнения Эрбрана–Геделя.Языки: Lisp, ML, Haskell.Логическое программирование : программа — это множествоформул, описывающих условия решаемой задачи.Математическая модель: логические исчисления.Языки: Prolog, Godel.ПАРАДИГМА ЛОГИЧЕСКОГОПРОГРАММИРОВАНИЯ''$ОПИСАНИЕ ЗАДАЧИПРОГРАММАДекларативная семантика&'$Операционная семантика%&$ОПИСАНИЕ ЗАДАЧИ = ПРОГРАММАДекларативнаясемантика&⇐⇒Операционнаясемантика%%ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫСинтаксис логических программПусть σ = hConst, Func, Predi — некоторая сигнатура, вкоторой определяются термы и атомы.«заголовок» ::= «атом»«тело» ::= «атом» | «тело», «атом»«правило» ::= «заголовок» ← «тело»;«факт» ::= «заголовок»;«утверждение» ::= «правило» | «факт»«программа» ::= «пусто» | «утверждение» «программа»«запрос» ::= | ? «тело»ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПримерыПравило: L(паша, Y ) ← L(Y , X ), L(паша, X );|{z}|{z}заголовоктелоФакт: L(даша, саша);Запрос (целевое утверждение ):? Умный(X ), Добрый(X ), Красивый(X ), Любит(X , меня)|{z} |{z} |{z} |{z}подцельподцельЗдесь X — целевая переменная .подцельподцельХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПример логической программы...P : elem(X , X L);elem(X , Y L) ← elem(X , L);concat(nil, Y , Y );concat(U X , Y , U Z ) ← concat(X , Y , Z );common(X , Y ) ← elem(U, X ), elem(U, Y );.и запроса к ней.