ЛМвИИ (1086253), страница 12
Текст из файла (страница 12)
Но при добавлении в множество Sдизъюнкта ¬R(x) вершина 2 становится неблагоприятной. Рассматривая теперьнеблагоприятные вершины 2 и 3, в которых невыполнимы дизъюнкты ¬R(x) и R(x)соответственно, можно, рассуждая аналогично, сделать вывод, что удовлетворить одновременноэтим вершинам может только пустой дизъюнкт. Для этого пустого дизъюнкта неблагоприятнойвершиной является вершина 1.Графически процесс вывода можно представить (рис.2.4) в виде дерева вывода, вкотором листья соответствуют исходному множеству дизъюнктов S, а прочие вершинысоответствуют выводимым дизъюнктам (резольвентам).Другими словами, если в дизъюнктах C1 и С2 есть атомы Р и ¬Р соответственно, то онивычеркиваются, а остатки дизъюнктов объединяются и получается резольвента. Обратимвнимание на то, что при переходе от семантических деревьев к деревьям вывода мы переходимот рассмотрения фундаментальных реализаций дизъюнктов к дизъюнктам, у которых термымогут содержать переменные, т.е.
к наиболее общему случаю.Рис. 2.4. Дерево выводаИнтерес представляет свойство заверши мости метода резолюции: конечное множествоS невыполнимо тогда и только тогда, когда пустой дизъюнкт может быть выведен из S спомощью резолюций. Из леммы 1 (§1.6) следует достаточность этого условия. Необходимостьусловия отражается в следующей лемме.Лемма 2.
Если множество дизъюнктов S невыполнимо и содержит резольвенты своихэлементов, то оно обязательно содержит пустой дизъюнкт.Иными словами, если множество S не пусто и не содержит ни одной пары дизъюнктов,допускающих резольвенту, то оно выполнимо.При рассмотрении семантических деревьев мы пользовались тем, что пара предикатов¬R(x) и R(x) противоречива. Переменная х может быть заменена на константу а и противоречиевысказываний ¬R(a) и R(a) становится очевидным. Вопрос, являются ли противоречивыми,скажем, предикаты ¬Р(х, f(х)) и Р(b, y) более сложен.
На такой вопрос дает ответ процедураунификации.Подстановкой будем называть конечное множество парπ ={t1 | v1, t2 | v2, …, tn | vn},где vi - индивидные переменные, все vi различны, ti - термы, отличные от vi ( ti заменяетпеременную vi).Литерал L'=Lπ, полученный заменой в литерале L переменных vi на термы ti, L'назовется конкретизацией L.Например, пусть π = {a | x, f(z) | y, b | z}, то P(x, y, z)π = P(a, f(z), b).Обозначим π3 = π2oπ1 композицию подстановок, результат применения которойсовпадает с результатом последовательно примененных подстановок π2 и π1Определим подстановку π3 = π2oπ 1 через подстановкиπ 1={t1 | x1, t2 | x2, …, tn | xn} и π2 ={s1 | y1, s2 | y2, …, sm | ym}.Нетрудно заметить, что π3 можно получить из множества{t1 π2| x1, t2 π2| x2, …, tn π2| xn ; s1 | y1, s2 | y2, …, sm | ym};исключив пары ti π2| xi , у которых ti π2 = хi , и такие пары si | yi , у которых y i ∈ { x 1 ,...
, x n } .Например, пусть π 1={z | x, w | y, f(x) | z} и π2 ={a | x, f(y) | z, y | w}. В этих обозначенияхимеем x1=x, x2=y, x3=z, y1=x, y2=z, y3=w. Тогда {t1 π2| x1, t2 π2| x2, t3 π2| x3, s1 | y1, s2 | y2, s3 | y3} ={f(y) | x, y | y, f(a) | z; a | x, f(y) | z, y | w}. Поскольку t2π2=x2, y1=x1, y2=x3, исключаем пары y | y,a | x, f(y) | z, получим π3 = π2oπ1 = {f(y) | x, f(a) | z, y | w}.Подстановку π называют унификатором множества {Li}, (i=1..n), если выполнение πприводит к равенству элементов множества L1π=L2π=...=Liπ=...=Lnπ (i=1..n). Множество {Li},(i=1..n) унифицируемо, если для него существует унификатор. Когда один из термов естьпеременная или содержит переменную, но не сводится к ней, то унификация невозможна.Пусть даны литералы L1=P(a, x, f(g(y))), L2=P(z, f(z), f(u)) и подстановка π={а | z, f(a) | х,g(y) | u}.
Для подстановки π выполняется равенствоP(a, x, f(g(y)))π=P(z, f(z), P(u))π=P(a, f(a), f(g(y))).Следовательно, π - унификатор множества {L1, L2}.Например, пара дизъюнкций P(a, x)vP(b, y) и P(a, f(x))vP(x, f(b)) неунифицируемо.Говорят, что унификатор π является более общим, чем унификатор σ, если существуеттакая подстановка τ, что σ=πoτ .Унификатор π называется наиболее общим унификатором (НОУ) тогда и толькотогда, когда для каждого унификатора σ существует подстановка τ такая, что σ=τoπ.Если π - НОУ для дизъюнктивной формулы A1vA2v...vAn , то атомарная формула В=A1π=A2π=...=Anπ называется фактором для A1vA2v...vAn .2.6.1.
Алгоритм унификации.Для нахождения НОУ используется алгоритм унификации, который за конечное числошагов определяет НОУ, если он существует.Два выражения Р(х) и Р(а) не тождественны. Они различаются аргументами. Эторазличие назовем рассогласованием и обозначим {х, а}. Дадим следующее определение:множеством рассогласований дизъюнктивной атомарной формулы P(v1(1), …, vn(1))vP(v1(2), …,vn(2))v...vP(v1(N), …, vn(N)) или короче - A1vA2v...vAN есть множество {t(1), t(2), …, t(N)}, котороеполучается следующим образом.Просматриваются все атомарные формулы Аi слева и выявляется первая позиция, накоторой не для всех Аi стоит один и тот же символ. Тогда для каждого i (1≤i≤N)рассогласование τ(i), есть различающиеся подвыражения из всех Ah начиная с этой позиции.Например, для дизъюнкцииP(x, g(f(y, z), x), y)vP(x, g(a, b), b)vP(x, g(g(h(x), a), y), h(x)) находим, просматривая слевацепочку символов, седьмую позицию, с которой символы различаются (подчеркнуто) и t(2) ={f(y, z), a, g(h(x), a)}.
Заметим, что множество рассогласований может содержать менее Nэлементов, так как не все t(i) должны быть отличающимися.Далее находится и выполняется подстановка π 1=(t | x), если множество рассогласованийсодержит переменную х и терм t, который не содержит х. В противном случае рассматриваемоемножество литер не унифицируемо. Аналогично находится и выполняется следующаяподстановка: π2, а результирующая подстановка равна композиции подстановок, найденных накаждом шаге работы алгоритма.Основная часть метода резолюции заключается в использовании алгоритмаунификации, который находит наиболее общий унификатор π для унифицируемойдизъюнктивной формулы и сообщении о завершении, если формула не унифицируема.Последовательность шагов алгоритма унификации следующая. Пусть задана дизъюнктивнаяформула А или задано множество дизъюнктов, подлежащих унификации, т.е.
полученияфактора для формулы А.Шаг 1. AK = A, k=0, подстановка αK = α0.Шаг 2. Если АK - фактор (единичный дизъюнкт), то αK - НОУ и процедура завершается.Иначе формируем множество рассогласований DK для АK.Шаг 3. Если существуют такие vK и tK в DK , что vK - индивидная переменная, невходящая в tK, то перейти к шагу 4. В противном случае - формула (множество) А неунифицируема, процедура завершается.Шаг 4. αK+1 = αK{tK | vK} и AK+1 = AK{tK | vK}, k=k+1. Перейти к шагу 2.Пример.
Найти НОУ для множестваL = {P(a, x, f(g(y))), P(z, f(z), f(u))}.На первом шаге имеем множество рассогласований D1 = {a, z} и подстановкуα1 = (а | z).В результате выполнения подстановки получаем множество литерL1 = Lα1 = {P(a, x, f(g(y))), P(a, f(a), f(u))}.На втором шаге имеем D2 = {x, f(a)}, α2 = {f(a) | x} иL2 = L1α2 = {P(a, f(a), f(g(y))), P(a, f(a), f(u))}.На третьем и последнем шаге имеем D3 = {g(y), u}, а3 = {g(y) | u}L3 =L2α3 = {P(a, f(a), f(g(y)))}.В результате найдем НОУ множестваπ = α3oα2oα1 = {a | z, f(a) | x, g(y) | u}.Пример. Найти НОУ для дизъюнкцииР(f(а), g(x))vP(y, у) или короче - A1vА2.Начнем с α0 = {} - пустая подстановка.
Множество рассогласований для A=A1vА2 естьD0 = {f(a), y}. Из этого следует v0 = y, t0 = f(а). Формируем подстановку α1 = {f(a) | y}.После подстановки дизъюнкция принимает вид:Аα1 = А1α1vА2α1 = P(f(a), g(x))vP(f(a), f(a)).Рассогласование для Аα1 есть D1 = {g(x), f(a)}.В D1 нет элемента, который мог бы быть переменной. Поэтому алгоритм унификациизавершается; делаем заключение -исходный дизъюнкт А не унифицируем.1.2.Унификация используется для решения двух задач :Унифицирует одноименные предикаты из разных дизъюнктов, отличающиеся наличиемотрицания. В результате становится возможным получение резольвенты.Унифицирует одноименные предикаты из одного дизъюнкта, имеющие одинаковыйзнак. В результате становится возможным получение частного случая для данногодизъюнкта (фактора). Факторы - это резольвенты, полученные на базе одногодизъюнкта.Так, из дизъюнкта R(х, у)vR(a, f(х))vR(х, х) можно получить факторыR(a, f(a))vR(a, a)R(x, x)vR(a, f(x)).Приведем следующие важные для дальнейшего понимания правил резолюцииопределения.Определение 1.
Если две или более литер (с одинаковы знаком) дизъюнкта А имеютнаиболее общий унификатор НОУ σ, то Аσ называется склейкой А. Если Аσ - единичныйдизъюнкт, то склейка называется единичной.Пример. Пусть A = P(x)vP(f(y))v¬Q(x). Тогда подчеркнутые литеры имеют НОУσ = {f(y) | x}. Следовательно, Aσ = P(f(y))v¬Q(f(y)) - склейка А.Определение 2. Пусть А1 и А2 - два дизъюнкта (посылки), которые не имеют общихпеременных. Пусть С1 и C2 две литеры из А1 и А2 соответственно. Если С1 и C2 имеют НОУ σ, тодизъюнкт (A1σ-C1σ)v(A2σ-C2σ) называется бинарной резольвентой А1 и А2. Литеры С1 и C2 отрезаемые литеры.Пример.A1 = P(x)vQ(x), A2 = ¬P(a)vR(x).Так как х входит в А1 и А2, то заменим х в А2 и пусть А2 = ¬P(a)vR(y).
Выберем С1 = P(x)и C2 = ¬P(a). НОУ для этих литер есть σ = {a | х}. Следовательно,(A1σ-C1σ)v(A2σ-C2σ) = ({P(a), Q(a)}-{P(a)}v{¬P(a), R(y)}-{¬P(a)}) = {Q(a)vR(y)} = Q(a)vR(y).Дизъюнкт Q(a)vR(y) ~ бинарная резольвента, а Р(х) и ¬Р(а) - обрезаемые литеры.2.6.2. Правило резолюций.Метод резолюции для доказательства выводимости теоремы из множества Sдизъюнктов основан на применении (возможно неоднократном) правила резолюции, состоящегоиз последовательных действий, приведенных ниже. Это правило, представляющее содержаниеметода резолюции, является отражением леммы, сформулированной в начале раздела. Посуществу правило резолюций есть последовательность шагов логического вывода,порождающего резольвенты для множествадизъюнктов.Лучшей иллюстрацией применения этого правила являются примеры, в которыхподробно рассматривается последовательность действий.Сформулируем основные положения:1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
