Автоматическое доказательство теорем. Метод резолюций

Пусть имеется множество формул Г = { A ₁, A ₂, …, A_n } и формула B. Автоматическим доказательством теоремы B называют алгоритм, который проверяет вывод A ₁, A ₂, …, A_n ⊢ B. Выражение читается следующим образом: "Если посылки A ₁, A ₂, …, A_n истинны, то истинно заключение B ".

Проблема доказательства в логике состоит в том, чтобы установить, что если истинны формулы A ₁, A ₂, …, A_n, то истинна формула B. Доказательство этого равносильно доказательству общезначимости некоторой формулы. Наиболее эффективно доказательство общезначимости формул осуществляется методом резолюций. Процедура поиска доказательства методом резолюций фактически является процедурой поиска опровержения, т. е. вместо доказательства общезначимости формулы доказывается, что отрицание формулы противоречиво.

При изложении метода резолюций обычно употребляется следующая терминология.

Литерой называется выражение A или Ø A. Литеры A и Ø A называются контрарными, а множество { A, Ø A } – контрарной парой.

Дизъюнкт – это дизъюнкция литер (или элементарная дизъюнкция). Дизъюнкт называется пустым, (обозначается ), если он не содержит литер. Пустой дизъюнкт всегда ложен, так как в нем нет литер, которые могли бы быть истинными при любых наборах переменных.

Рассмотрим применение метода резолюций к исчислению высказываний.

Правилом резолюции называют следующее правило вывода:

Правило резолюции можно записать в следующем виде: A Ú B, Ø A Ú C ⊢ B Ú C.

Дизъюнкт B Ú C называется резольвентой дизъюнктов A Ú B и Ø A Ú C по литере A: B Ú C = res_A (A Ú B и Ø A Ú C).

Если дизъюнкты не содержат контрарных литер, то резольвенты у них не существует. Для дизъюнктов A и Ø A резольвента есть пустой дизъюнкт: res_A (A, Ø A) = .

Пример 3.4.

Пусть F = A Ú B Ú C, G = Ø A ÚØ B Ú D.

Тогда

res_A (F, G) = B Ú C Ú Ø B Ú D.

res_B (F, G) = A Ú C ÚØ A Ú D.

res_C (F, G) не существует.

Метод резолюций соответствует методу доказательства от противного. Условие A₁, A₂, …, A_n ⊢ B равносильно условию A ₁, A ₂,…, A_n, Ø B ⊢ .

Алгоритм построения вывода методом резолюций.

Шаг 1. Все формулы посылок A₁, A₂, …, A_n и формулу отрицания заключения Ø B привести к КНФ.

Шаг 2. Выписать множество K дизъюнктов всех посылок A₁, A₂, …, A_n и отрицания заключения Ø B: K= { D₁, D₂, …, D_n }.

Шаг 3. Выполнить анализ пар множества K правилу: если существуют дизъюнкты D_i, D_j, один из которых D_i, содержит переменную A_i, а другой D_j –отрицание Ø A_i, то соединить эту пару логической связкой дизъюнкции D_i Ú D_j и сформировать по правилу резолюции новый дизъюнкт – резольвенту, исключив содержащих контрарные литеры A_i и Ø A_i.

Шаг 4. Процесс продолжаем. Если он заканчивается пустым дизъюнктом, то вывод обоснован.

Изложенный алгоритм назывется резолютивным выводом из K.

Возможны три случая.

1. Среди множества дизъюнктов нет содержащих контрарные литеры. Это означает, что формула B не выводима из множества формул A ₁, A ₂, …, A_n.

2. После очередного применения правила резолюции получен пустой дизъюнкт. Это означает, что формула B выводима из множества формул A ₁, A ₂,…, A_n.

3. Процесс зацикливается, т. е. получаются все новые резольвенты, среди которых нет пустых.

Пример 3.5.

Применить для примера 3.2 A ® (B ® C), A Ù B ⊢ C метод резолюций. Для этого нужно проверить вывод A ® (B ® C), A Ù B, Ø C ⊢ .

Алгоритм решения.

Шаг 1. Привести к КНФ формулы A ® (B ® C), A Ù B, Ø C.

A ®(B ® C) º Ø A Ú(B ® C) º Ø A ÚØ B Ú C.

Формулы A Ù B, Ø C уже находятся в КНФ.

Шаг 2. Составим множество К дизъюнктов:

К = {Ø A Ú Ø B Ú C, A, B, Ø C }.

Шаг 3. Построим резолютивный вывод из K. Выпишем по порядку все дизъюнкты из K:

1) Ø A Ú Ø B Ú C;

2) A;

3) B;

4) Ø C;

Вместо пары дизъюнктов, содержащих контрарные литеры запишем их резольвенту (в скобках указаны номера формул, образующих резольвенту):

5) Ø B Ú C. (1, 2)

6) C. (3, 5)

7) . (4, 6)

Вывод заканчивается пустым дизъюнктом, что является обоснованием вывода A ® (B ® C), A Ù B ⊢ C.

Задания

1. Установить правильность рассуждения, построив вывод исчисления высказываний.

2. Проверить вывод методом резолюций.

Варианты индивидуальных заданий

Вариант № 1

1. На работу в эту организацию принимают, если пройдешь собеседование и будешь аттестован положительно. Его не приняли. Значит, он либо не прошел собеседование, либо не был положительно аттестован.

2. X, B, (C Ù X)®Ø B ⊢ C.

Вариант № 2

1. Если светофор красный, то проезд не разрешен. Проезд разрешен. Значит, светофор не красный.

2. Ø A ® (B Ú C), Ø A Ú C, Ø B ⊢ C.

Вариант № 3

1. Если треугольник равносторонний, то его углы равны. Треугольник равносторонний. Следовательно, его углы равны.

2. ((X Ù C) ® Ø B) ⊢ Ø C.

Вариант № 4

1. Если ограбление совершил Сидоров, то он знает, где находятся похищенные деньги. Сидоров не знает, где находятся похищенные деньги. Следовательно, он не совершал ограбления.

2. A Ú F, A ® C, F ® D ⊢ C Ú D.

Вариант № 5

1. Если растение лекарственное, его следует охранять. Это растение не подлежит охране. Следовательно, оно не лекарственное.

2. A, C, (A Ù C)® D, D ® F ⊢ F.

Вариант № 6

1. Петров инженер или студент. Он не инженер. Следовательно, он студент.

2. Ø A ® (B Ú C), A ® B, Ø C ⊢ B.

Вариант № 7

1. Если студент занимается не систематически, то он не имеет прочных знаний. Если он не имеет прочных знаний, то он не будет хорошим специалистом. Следовательно, если студент занимается не систематически, то он не будет хорошим специалистом.

2. A, A ® (Ø B ® C), B ® D, Ø C ⊢ D.

Вариант № 8

1. Это вещество может быть кислотой либо солью. Это вещество не соль. Следовательно, это кислота.

2. (A ® C) ® (Ø A ® B)⊢ A Ú B.

Вариант № 9

1. Если прямая касается окружности, то радиус, проведенный в точку касания, перпендикулярен к ней. Радиус окружности не перпендикулярен к этой прямой. Следовательно, прямая не касается окружности.

2. F Ú C, C ® A, F ® D, D ® A ⊢ A.

Вариант № 10

1. Если человек знает геометрию, то он знает теорему Пифагора. Этот человек не знает теорему Пифагора. Следовательно, он не знает геометрию.

2. Ø B ® (D ® C), D, C ® (A Ú B)⊢ A Ú B.

Вариант № 11

1. Если слово ставится в начале предложения, то оно пишется с большой буквы. Это слово написано с маленькой буквы. Следовательно, это слово не стоит в начале предложения.

2. B ® (C ® A), Ø B ® D, D ® C, ⊢ C.

Вариант № 12

1. Если функция четная, то ее график симметричен относительно оси OY. График несимметричен относительно оси OY. Следовательно, функция не является четной.

2. B ® (C ® A), Ø B ® E, C, Ø E ⊢ A

Вариант № 13

1. Если светофор зеленый, то проезд разрешен. Проезд не разрешен. Значит, светофор не зеленый.

2. Ø C, D ® C, A ® (Ø B ® D), B ⊢ A ® C.

Вариант № 14

1. Если Андрей отсутствовал на работе, он не выполнил задания. Андрей был на работе. Следовательно, он выполнил задание.

2. C ® (B ® A), Ø B ® E, C ⊢ A Ú E.

Вариант № 15

1. Плох тот солдат, который не мечтает стать генералом. Этот солдат хорош. Следовательно, он мечтает стать генералом.

2. A ® (C ® B), D ® A, C ⊢ D ® B.

Вариант № 16

1. Если треугольник равносторонний, то он равнобедренный. Если треугольник равнобедренный, то углы при основании равны. Следовательно, если треугольник равносторонний, то углы при основании равны.

2. A, X ® C ⊢ (A ® Ø C) ® Ø X.

Вариант № 17

1. Если диагноз подтвердится, то ему придется лечь в больницу. Если он ляжет в больницу, то поездку придется отменить. Диагноз подтвердился. Значит, поездку придется отменить.

2. A ® (C ® B), D ® A, C ⊢ D ® B.

Вариант № 18

1. Петров студент или школьник. Он не школьник. Следовательно, он студент.

2. A, A ® (B ® C), Ø B ® D, Ø C ⊢ D.

Вариант № 19

1. Если я устал, то не могу готовиться к занятиям. Если я не смогу приготовиться к занятиям, я не напишу контрольную работу. Я устал. Значит, я не напишу контрольную работу.

2. B ® (E ® C), E, C ® (A Ú Ø B) ⊢ B ® A.

Вариант № 20

1. Если Сергей победит на соревнованиях, он войдет в сборную страны. Если он войдет в сборную страны, то будет участвовать в чемпионате мира. Следовательно, если Сергей победит на соревнованиях, он будет участвовать в чемпионате мира.

2. G ® (B Ú C), G Ú C, Ø B ⊢ C.

Тема 4. НЕЧЕТКАЯ ЛОГИКА

Нечеткая логика отличается от двузначной классической логики тем, что если значения истинности высказывания классической логики могут быть только 0 («ложь») и 1 («истина»), то нечеткая логика допускает несчетное число промежуточных истинностных значений для высказываний в интервале [0, 1].

При описании сложных систем, в которых наряду с количественными данными присутствуют неоднозначные качественные данные, приходится использовать нечеткие понятия и рассуждения. Для формализации таких задач Л. Заде разработал основы математического аппарата, опирающегося на понятия нечетких множеств и нечеткой логики.

Основные понятия нечетких множеств

Пусть М – некоторое множество, рассмотрим какое-либо подмножество А этого множества. Для любого х Î М имеем х Î А или х Ï А. Можно ввести характеристическую функцию подмножества А:

Тогда, например, если M= { a, b, c, d, e, f, g, h }и A= { a, b, c, d }, имеем:

x	а	b	с	d	е	f	g	h
m_A (x)

Для универсального множества М: "х m_M (x) = 1.

Множества, для которых характеристическая функция принимает только значения 0 или 1, будем называть четкими. Классическая логика оперирует с четкими множествами.

Для нечетких множеств характеристическая функция может принимать любые значения из интервала [0,1]. Например,

x	а	b	с	d	е	f	g	h
m_A (x)	1,0	0,1	0,8	0,7	0,5	0,2	0,0	0,1
m_B (х)	0,1	0,3	0,8	0,9	0,5	0,1	0,0	0,0

Для записи нечетких множеств используется обозначение: А= {(х, m_A (х)) | " x Î M }. Запись характеризует степень принадлежности элемента x множеству A.

Для нечетких множеств определены отношение включения (Ì) и равенства (=):

А Ì В тогда и только тогда, когда " x Î M: m_A (х) £ m_B (х);

А = В тогда и только тогда, когда " x Î M: m_A (х) = m_B (х).

Над нечеткими множествами выполняются операции:

Дополнение А:

Пересечение:

Объединение:

А È В= {(х, max { m_A (х), m_B (х)})| "xÎ M }.

Элементы нечеткой логики

Нечетким высказыванием называется высказывание P, степень истинности которого m_P можно оценить числом из интервала [0, 1], m_P Î [0, 1].

Нечеткой высказывательной переменной X называется нечеткое высказывание X, степень истинности которого может меняться в интервале [0, 1].

Так как степень истинности нечеткого высказывания не связана с сутью высказывания, будем в дальнейшем отождествлять нечеткое высказывание с его степенью истинности аналогично тому, как обычное четкое высказывание отождествлялось с его истинностью или ложностью. Нечеткие высказывания и степень их истинности будем обозначать буквами: P, Q, X, и т. д.

На множестве нечетких высказываний вводятся логические операции, аналогичные операциям алгебры высказываний.

1. Отрицание нечеткого высказывания:Ø P = 1 – P.

2. Конъюнкция нечетких высказываний: P Ù Q = min (P, Q).

3. Дизъюнкция нечетких высказываний: P Ú Q = max (P, Q).

4. Импликация нечетких высказываний: P ® Q = max (1 – P, Q).

5. Эквивалентность нечетких высказываний:

P «Q = min (max (1 – P, Q), max (P, 1 – Q)).

Пример 4.1.

Найти степень истинности высказывания

R = (P Ú Q) «(P ® (P Ù Q)) при P = 0,9; Q = 0,3.

1. P Ù Q = min (0,9; 0,3) = 0,3.

2. (P ® (P Ù Q)) = max (1 – 0,9; 0,3) = 0,3.

3. P Ú Q = max (0,9; 0,3) = 0,9.

4. R = min (max (1 – 0,9; 0,3), max (0,9; 1 – 0,3)) = min (0,3; 0,9) = 0,3.

Множество нечетких высказываний вместе с введенными на них операциями образуют алгебру нечетких высказываний.

Нечеткой логической формулой называется:

1) любая нечеткая высказывательная переменная;

2) если P и Q – нечеткие логические формулы, то Ø P, P Ù Q, P Ú Q, P ® Q, P «Q – тоже нечеткие логические формулы;

3) других формул, кроме построенных по правилам двух предыдущих пунктов, нет.

Пусть P (X ₁, X ₂, …, X_n) и Q (X ₁, X ₂, …, X_n) – две нечеткие логические формулы. Степенью равносильности формул P и Q называется величина

m (P, Q) = { P (a₁, a₂, …,a _n) «Q (a₁, a₂, …,a _n)}

Здесь логические операции конъюнкции и эквивалентности имеют смысл, определенный для логических операций над нечеткими высказываниями, причем конъюнкция берется по всем наборам степеней истинности (a₁, a₂, …,a _n) нечетких переменных (X ₁, X ₂, …, X_n).

Если m (P, Q) = 0,5, то нечеткие формулы P и Q называются индифферентными.

Если m (P, Q) > 0,5, то нечеткие формулы P и Q называются нечетко равносильными.

Если m (P, Q) < 0,5, то нечеткие формулы P и Q называются нечетко неравносильными.

Степенью неравносильности формул P и Q называется величина

(P, Q) = 1 – m (P, Q).

Пример 4.2.

Определить степень равносильности формул.

P = X ® Y, Q = Ø(X Ù Y) при условии, что X и Y принимают значения степеней истинности из множества {0,1; 0,3}. Перечислим все возможные наборы значений X и Y:

A₁ = {0,1; 0,1}; A₂ = {0,1; 0,3}; A₃ = {0,3; 0,1}; A₄ = {0,3; 0,3}.

Запишем формулы P и Q с учетом определений логических операций:

P = X ® Y = max (1 – X, Y); Q =Ø(X Ù Y) = 1 – X Ù Y = 1 – min (X, Y).

Вычислим формулы P и Q на каждом из четырех наборов A ₁– A ₄:

P₁ = max (1 – 0,1; 0.1) = 0,9. P₂ = max (1 – 0,1; 0,3) = 0,9. P₃ = max (1 – 0,3; 0,1) = 0,7. P₄ = max (1 – 0,3; 0,3) = 0,7.

Q₁ = 1 – min (0,1; 0.1) = 0,9. Q₂ = 1 – min (0,1; 0,3) = 0,9. Q₃ = 1 – min (0,3; 0,1) = 0,9. Q₄ = 1 – min (0,3; 0,3) = 0,7.

Вычислим теперь степень равносильности формул P и Q. Для этого сначала вычислим P (a₁, a₂, …, a_n) «Q (a₁, a₂, …, a_n) для всех наборов A ₁– A ₄:

P «Q = min (max (1 – P, Q), max (P, 1 – Q)).

Поэтому

P₁ «Q₁ = min (max (1 – 0,9;0,9), max (0,9; 1 –0,9)) = 0,9.

P₂ «Q₂ = min (max (1 – 0,9;0,9), max (0,9; 1 –0,9)) = 0,9.

P₃ «Q₃ = min (max (1 – 0,7;0,9), max (0,7; 1 –0,9)) = 0,7.

P₄ «Q₄ = min (max (1 – 0,7;0,8), max (0,7; 1 –0,7)) = 0,7.

Окончательно получим

m (P, Q) = { P (a₁, a₂, …,a _n) «Q (a₁, a₂, …,a _n)} = 0,9Ù0,9Ù0,7Ù0,7 = min (0,9; 0,9; 0,7; 0,7) = 0,7.

Формулы P и Q нечетко равносильны.

На других наборах степеней истинности нечетких переменных X и Y формулы P и Q могут быть нечетко неравносильны.

Задания

Определить степень равносильности формул P и Q при условии, что X и Y принимают значения степеней истинности из множества {0,1; 0,5}.

Варианты индивидуальных заданий

№	P	Q	№	P	Q
	X ÙØ Y	X ®Ø Y		ØX Ú Y	X ÙØ Y
	ØX Ú Y	X ® Y		X ® Y	ØX Ú Y
	X ®Ø Y	X ÙØ Y		X ÙØ Y	X ®Ø Y
	X Ù Y	X Ú Ø Y		X ®Ø Y	X Ù Y
	X Ú Ø Y	Ø X Ù Y		Ø X Ù Y	X Ú Ø Y
	X ® Y	ØX Ú Y		X Ú Ø Y	X ® Y
	Ø X ® Y	Y ® X		Y ® X	Ø X ® Y
	Y ®Ø X	Ø X ® Y		Ø X ® Y	Y ®Ø X
	Ø Y ® X	Y ®Ø X		Y ®Ø X	Ø Y ® X
	Ø Y ®Ø X	Y ® X		Y ® X	Ø Y ®Ø X