а) Если y – формула языка L, то вывод 墢 
y существует тогда и только тогда в L¢¢, когда существует вывод å y в L
б) Теория å непротиворечива, если и только если непротиворечива теория 墢.
Метод резолюций Робинсона
В предыдущем разделе мы научились приводить формулы к виду, пригодному для применения метода автоматического доказательства теорем, предложенного в 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.
Нечеткая логика
Многие понятия, определяемые с помощью человеческого языка, являются расплывчатыми. Например, попытка дать определение кучи камней приводит к следующей антиномии: «Один или два камня – не куча; с другой стороны, если из кучи удалить камень, то куча останется».
Л. Заде предложил приписывать объектам степень выполнения определяемого свойства, принимающую значения в единичном интервале [0, 1]. Эта идея была положена в основу теории нечетких множеств. Она позволила моделировать человеческие рассуждения и операции над нечеткими свойствами объектов.
Нечеткие множества
Пусть U – произвольное множество. Будем рассматривать его подмножества и U будем называть универсумом. Каждое подмножество описывается с помощью свойств его элементов. Например, в универсуме натуральных чисел w подмножество
{0, 1, 2, 3, 4, 5} задаётся как
A = {n Î w: n £ 5}.
Его можно определить с помощью характеристической функции 
, принимающей значения:
Проблема возникает при попытке определения подмножества чисел, указывающих значение возраста, при которых человек считается старым.
Пусть [0, 1] = {r Î R: 0 £ r £ 1} – единичный отрезок действительных чисел.
Определение. Нечетким множеством m на универсуме U называется произвольная функция m: U ® [0, 1]. Множество всех нечетких множеств на U обозначается через F(U).
Заметим, что часто понятия нечёткого множества и определяющей его функции различают. В этом случае, говоря о нечётком множестве A, имеют в виду функцию 
. Обозначают эту функцию через 
и называют её функцией принадлежности.
Значение m(x) называется степенью принадлежности x нечеткому множеству m. Например, нечеткое множество «старый» определяется как функция 
, для которой m(70) = 1, а m(0) = 0, ибо ясно, что человек семидесяти лет является старым, а не достигнувший одного года младенец – нет. Можно считать, что m(20) = 0. Возрасту 45 лет можно приписать значение m(45) = 0.5, и далее продолжить функцию m линейно на интервале [20, 70].
