Теорема (вторая e-теорема)

а) Если y – формула языка L, то вывод 墢 Теорема (вторая e-теорема) - student2.ru y существует тогда и только тогда в L¢¢, когда существует вывод å Теорема (вторая e-теорема) - student2.ru y в L

б) Теория å непротиворечива, если и только если непротиворечива теория 墢.

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

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

Задача ставится так: заданы язык первого порядка L и конечное множество аксиом å. Требуется найти вывод å Теорема (вторая e-теорема) - student2.ru 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,

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

Если D1 и D2 – дизъюнкты, для которых существуют такие дизъюнкты Теорема (вторая e-теорема) - student2.ru и литерал В, что Теорема (вторая e-теорема) - student2.ru и Теорема (вторая e-теорема) - student2.ru , то формула:

Теорема (вторая e-теорема) - student2.ru

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

правило конъюнкции Теорема (вторая e-теорема) - student2.ru (Con) и правило резолюции Теорема (вторая e-теорема) - student2.ru (Res)

Предположим, что требуется доказать вывод q1, q2, …, qn Теорема (вторая e-теорема) - student2.ru q. Сведём задачу к доказательству противоречивости формулы q1 & q2 & …& qn & Øq. Приведём последнюю к конъюнктивной нормальной форме. Получим конъюнкцию некоторых дизъюнктов, составляющих список:

D1, D2, …, Dk.

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

Пример 1

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

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

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

Ø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, которые имеют наибольший общий унификатор и Теорема (вторая e-теорема) - student2.ru , Теорема (вторая e-теорема) - student2.ru для некоторых дизъюнктов Теорема (вторая e-теорема) - student2.ru и Теорема (вторая e-теорема) - student2.ru . В этом случае резольвента определяется как

Теорема (вторая e-теорема) - student2.ru .

Здесь 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 Теорема (вторая e-теорема) - student2.ru 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) Теорема (вторая e-теорема) - student2.ru 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}.

Его можно определить с помощью характеристической функции Теорема (вторая e-теорема) - student2.ru , принимающей значения:

Теорема (вторая e-теорема) - student2.ru

Проблема возникает при попытке определения подмножества чисел, указывающих значение возраста, при которых человек считается старым.

Пусть [0, 1] = {r Î R : 0 £ r £ 1} – единичный отрезок действительных чисел.

Определение. Нечетким множеством m на универсуме U называется произвольная функция m : U ® [0, 1]. Множество всех нечетких множеств на U обозначается через F(U).

Заметим, что часто понятия нечёткого множества и определяющей его функции различают. В этом случае, говоря о нечётком множестве A, имеют в виду функцию Теорема (вторая e-теорема) - student2.ru . Обозначают эту функцию через Теорема (вторая e-теорема) - student2.ru и называют её функцией принадлежности.

Значение m(x) называется степенью принадлежности x нечеткому множеству m. Например, нечеткое множество «старый» определяется как функция Теорема (вторая e-теорема) - student2.ru , для которой m(70) = 1, а m(0) = 0, ибо ясно, что человек семидесяти лет является старым, а не достигнувший одного года младенец – нет. Можно считать, что m(20) = 0. Возрасту 45 лет можно приписать значение m(45) = 0.5, и далее продолжить функцию m линейно на интервале [20, 70].

Наши рекомендации