4.7. Метод резолюций Робинсона

В предыдущем разделе мы научились приводить формулы к виду, пригодному для применения метода автоматического доказательства теорем, предложенного в 1965 году Робинсоном.

Задача ставится так: заданы язык первого порядка L и конечное множество аксиом å. Требуется найти вывод å  q для произвольной формулы q.

Она решается методом резолюций. Идею этого метода продемонстрируем сначала для случая, когда L – исчисление высказываний с множеством пропозициональных символов Р.

Алфавит исчисления состоит из элементов множества P и символов констант 0 (ложь) и 1 (истина), а также логических символов (, ), &, Ú, Ø.

Формулы определяются по индукции

1. Каждый символ из P – формула.

2. Константы 0 и 1 – формулы.

3. Если A и B – формулы, то (A&B), (AÚB), (ØA) – формулы.

Аксиомы.

(R1)       Ø0 = 1,

(R2)       A & B = B & A, A Ú B =  BÚA,

(R3)       A &1 = A, A Ú 1 = 1, A & 0 = 0, A Ú 0 = A,

(R4)       Ø(A & B) = ØA Ú ØB, Ø(A Ú B) = ØA & ØB,

(R5)       A & (B Ú C) = (A & B) Ú (A & C), A Ú (B & C) = (A Ú B) & (A Ú C),

(R6)       ØØA = A,

Правила вывода. Напомним, что для каждого символа А Î Р символы А и ØА называются литералами. Клоусом, или дизъюнктом называется дизъюнкция литералов .

Если D1 и D2 – дизъюнкты, для которых существуют такие дизъюнкты  и литерал В, что  и , то формула:

называется резольвентой D1 и D2. Таким образом, имеем

правило конъюнкции  (Con) и правило резолюции (Res)

Предположим, что требуется доказать вывод q1, q2, …, qn  q. Сведём задачу к доказательству противоречивости формулы q1 & q2 & …& qn & Øq. Приведём послед

нюю к конъюнктивной нормальной форме. Получим конъюнкцию некоторых дизъюнктов, составляющих список:

D1, D2, …, Dk.

Далее в цикле перебираем пары дизъюнктов из этого списка, находим резольвенты  и добавляем эти резольвенты, которые, очевидно, будут дизъюнктами, в конец списка. Если в списке появится 0, то вывод доказан. Если новые дизъюнкты не могут быть построены, то вывода нет.

Пример 1

Пусть требуется установить выводимость a ® b  a Ú c ® b Ú c. Преобразуем в формулу высказываний, заменяя импликацию по формуле A®Bº ØAÚB. Получим формулу: Øa Ú b  Ø(a Ú c) Ú b Ú c, которую надо доказать. Будем доказывать противоречивость конъюнкции дизъюнктов:

Øa Ú b,   a Ú c, Øb, Øc.

Так как , то к списку добавляется дизъюнкт b Ú c. Затем добавим . Получим список:

Øa Ú b,   a Ú c, Øb, Øc, b Ú c, с.

Теперь Res (Øc, с) = 0 даёт противоречие. Значит, выводимость имеет место.

Рассмотрим теперь метод резолюций для нахождения вывода в исчислении предикатов. Мы видели, что можно предполагать формулы q и аксиомы из å, не имеющими кванторов. Для любых двух атомных формул Р(s1, …, sm) и Q(t1, …, tn) их наибольший общий унификатор h определён, если и только если P = Q, m = n, и система уравнений s1 = t1, s2 = t2, …, sn = tn  унифицируема. Литералами в исчислении предикатов называются атомные формулы и их отрицания. Дизъюнкт определяется как дизъюнкция литералов. Два дизъюнкта D1 и D2 называются резольвируемыми, если существуют литералы B1 и B2, которые имеют наибольший общий унификатор и ,  для некоторых дизъюнктов  и . В этом случае резольвента определяется как

.

Здесь h(D) – результат подстановки h в дизъюнкт D, определённый как h(R(t1, …, tn)) = = R(ht1, …, htn) для атомных формул, h(ØR) = Øh(R) для литералов, и h(B1 Ú … Ú Bn)= =h(B1) Ú … Ú h(Bn) для дизъюнктов.

Алгоритм доказательства выводимости q1, q2, …, qm  q, в предположении, что q и qi, 1 £ i £ m, не имеют кванторов, будет следующим:

1) формулу q1 & …& qm & Øq переводим в конъюнкцию дизъюнктов D1&D2&…&Dn, и переменные переименовываются таким образом, что Di и Dj не содержат одинаковых переменных при i ¹ j;

2) устанавливаем множество дизъюнктов:  F = {D1, D2, …, Dn}.

3) если среди элементов из F нет резольвируемых, то выводимость не имеет  места, заканчиваем работу;

4) если 0 Î F, то F противоречиво, а выводимость имеет место, заканчиваем работу;

5) берём резольвируемые дизъюнкты Di и Dj из F, устанавливаем:

F = F È {Res (Di, Dj)}

(этот шаг включает унификацию некоторых литералов), переходим к шагу 3.

Следующий пример принадлежит Робинсону.

Пример 2

Докажем выводимость P(a, b), Q(z)  P(xy) & Q(y). После переноса правой части в левую часть получаем множество дизъюнктов:

F = {P(ab), Q(z), ØP(xy) Ú ØQ(y)}.

Наибольший общий унификатор для P(ab) и P(xy) равен: {a = x, b = y}.

Добавим к F резольвенту:

Res (P(ab), ØP(xy) Ú ØQ(y)) = ØQ(y).

Имеем: F = {P(ab), Q(z), ØP(xy) Ú ØQ(y), ØQ(y)}. Резольвента Res (Q(z), ØQ(y)) = 0 приводит к противоречивости F. Стало быть, выводимость имеет место. Легко видеть, что для данного примера существуют другие пути применения метода резолюций.

Существуют различные модификации метода резолюций.

В методе резолюций участвует также правило склейки, оно позволяет из дизъюнкта R(s1, …, sn) Ú R(t1, …, tn) Ú B1 Ú … Ú Bm получить h(R(s1, …, sn) Ú B1 Ú … Ú Bm), (а из дизъюнкта ØR(s1, …, sn) Ú ØR(t1, …, tn) Ú B1 Ú … Ú Bm – дизъюнкт h(ØR(s1,…, sn)Ú Ú B1 Ú … Ú Bm)) , где h – наибольший общий унификатор системы уравнений s1 = t1, …, sn = tn.