Автоматическое доказательство теорем. Метод резолюций.
Пусть имеется множество формул Г = {A1, A2, …, An} и формула B. Автоматическим доказательством теоремы B называют алгоритм, который проверяет вывод
A1, A2, …, An ├ B. (3. 1)
Выражение (3.1) можно прочитать следующим образом:
Если посылки A1, A2, …, An истинны, то истинно заключение B.
или
Если причины A1, A2, …, An имели место, то будет иметь место следствие B.
Проблема доказательства в логике состоит в том, чтобы установить, что если истинны формулы A1, A2, …, An, то истинна формула B.
В общем случае такой алгоритм построить нельзя. Но для некоторых частных случаев такие алгоритмы существуют. Доказательство теоремы равносильно доказательству общезначимости некоторой формулы. Наиболее эффективно доказательство общезначимости формул осуществляется методом резолюций. Процедура поиска доказательства методом резолюций фактически является процедурой поиска опровержения, т. е. вместо доказательства общезначимости формулы доказывается, что отрицание формулы противоречиво:
A º И Û ØA º Л.
Введем терминологию, обычно употребляемую при изложении метода резолюций.
Литерой будем называть выражения A или ØA. Литеры A и ØA называются контрарными, а множество {A, ØA} – контрарной парой.
Дизъюнкт – это дизъюнкция литер (или элементарная дизъюнкция).
Пример 3.6.
A Ú B Ú C – дизъюнкт;
A Ú ØB – дизъюнкт;
A Ú B & C – не дизъюнкт;
ØA – дизъюнкт.
Дизъюнкт называется пустым, (обозначается ), если он не содержит литер. Пустой дизъюнкт всегда ложен, так как в нем нет литер, которые могли бы быть истинными при любых наборах переменных.
Рассмотрим применение метода резолюций к исчислению высказываний.
Правилом резолюции называют следующее правило вывода:
. (3. 2)
Правило (3.2) можно также записать в следующем виде:
AÚB, ØAÚC ├ B Ú C. (3. 3)
Правило резолюций можно доказать, используя равносильности логики высказываний:
(AÚB) & (ØAÚC) É (B Ú C) = Ø((AÚB) & (ØAÚC)) Ú (B Ú C) = Ø(AÚB) Ú Ø(ØAÚC) Ú (B Ú C) = ØA&ØB Ú A&ØC Ú (B Ú C) = (ØAÚ A) & (ØAÚ ØC) & (ØBÚ A) & (ØBÚ ØC) Ú (B Ú C) = (ØAÚ ØC) & (ØBÚ A) & (ØBÚ ØC) Ú (B Ú C) =(ØAÚ ØC Ú B Ú C) & (ØBÚ A Ú B Ú C) & (ØBÚ ØC Ú B Ú C) = И.
Итак, при истинных посылках истинно заключение.
Правило (3.2) – единственное правило, применяемое в методе резолюций, что позволяет не запоминать многочисленных аксиом и правил вывода.
Дизъюнкт BÚC называется резольвентой дизъюнктов AÚB и ØAÚC по литере A:
BÚC = resA(AÚB и ØAÚC).
Если дизъюнкты не содержат контрарных литер, то резольвенты у них не существует.
Для дизъюнктов A и ØA резольвента есть пустой дизъюнкт: resA(A, ØA) = .
Пример 3.7.
Пусть F = A Ú B Ú C, G = ØA Ú ØB Ú D.
Тогда
resA(F, G) = B Ú C Ú ØB Ú D.
resB(F, G) = A Ú C Ú ØA Ú D.
resC(F, G) не существует.
Метод резолюций соответствует методу доказательства от противного. Действительно, условие A1, A2, …, A ├ B равносильно условию A1, A2, …, An, ØB├ . Метод резолюций относится к методам непрямого вывода.
Изложим процедуру вывода A1, A2, …, An ├ B в виде алгоритма.
Алгоритм построения вывода методом резолюций.
Шаг 1. Формулы A1, A2, …, An и формулу ØB привести к КНФ.
Шаг 2. Составить множество S дизъюнктов формул A1, A2, …, An и ØB.
Шаг 3. Вместо пары дизъюнктов, содержащих контрарные литеры записать их резольвенту по правилу (3.2).
Шаг 4. Процесс продолжаем. Если он заканчивается пустым дизъюнктом, то вывод обоснован.
Изложенный алгоритм назывется резолютивным выводом из S.
Возможны три случая:
1. Среди множества дизъюнктов нет содержащих контрарные литеры. Это означает, что формула B не выводима из множества формул A1, A2, …, An.
2. В результате очередного применения правила резолюции получен пустой дизъюнкт. Это означает, что что формула B выводима из множества формул A1, A2, …, An .
3. Процесс зацикливается, т. е. получаются все новые и новые резольвенты, среди которых нет пустых. Это ничего не означает.
Пример 3.8.
В примере 3.3 а) был обоснован вывод 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. Составим множество S дизъюнктов:
S = {ØA Ú ØB Ú C, A, B, ØC}.
Шаг 3. Построим резолютивный вывод из S. Для этого выпишем по порядку все дизъюнкты из S:
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.
Пример 3.9.
Записать с помощью формул логики высказываний и решить методом резолюций следующую задачу:
«Чтобы хорошо учиться, надо прикладывать усилия. Тот, кто хорошо учится, получает стипендию. В данный момент студент прикладывает усилия. Будет ли он получать стипендию?
Введем следующие высказывания:
A = ”студент хорошо учится”.
B = ”студент прикладывает усилия”.
C = ”студент получает стипендию”
Чтобы утвердительно ответить на вопрос задачи: ”Будет ли студент получать стипендию?”, нужно проверить вывод:
B É A, A ÉC, B ├ C.
Будем действовать в соответствии с алгоритмом.
Шаг 1. Нужно привести к КНФ формулы B É A, A ÉC, B, ØC.
B É A = ØB Ú A,
A ÉC = ØA ÚC,
Формулы B и ØC уже находятся в КНФ.
Шаг 2. Составим множество S дизъюнктов:
S = {ØB Ú A, ØA ÚC, B, ØC}.
Шаг 3. Построим резолютивный вывод из S. Сначала перепищем по порядку дизъюнкты из S:
1) ØB Ú A.
2) ØA ÚC.
3) B.
4) ØC.
Затем вместо пары дизъюнктов, содержащих контрарные литеры запишем их резольвенту:
5) ØB Ú C. (1, 2)
6) C. (3, 5)
7) . (4, 6)
Таким образом, на вопрос задачи можно ответить утвердительно: ”Студент будет получать стипендию”.
Правило резолюций более общее, чем правило modus ponens и производные правила, рассмотренные в п. 3.2. Докажем методом резолюций правило modus ponens. Необходимо построить вывод
A, A É B ├ B.
Построим резолютивный вывод.
A, ØA Ú B ├ B.
A, ØA Ú B, ØB├ .
S = {A, ØA Ú B, ØB}.
1) A.
2) ØA Ú B.
3) ØB.
4) B. (1, 2)
5) . (3, 4)
Метод резолюций легко поддается алгоритмизации. Это позволяет использовать его в логических языках, в частности в ПРОЛОГе. Недостатком этого метода является необходимость представления формул в КНФ. Кроме того, автоматическое доказательство теорем методом резолюций основан на переборе и этот перебор может быть настолько большим, что затраты времени на него практически неосуществимы. Эти обстоятельства стимулируют поиски различных модификаций метода резолюций.
Приведем еще один пример применнения метода резолюций, основанного на попарном переборе дизъюнктов.
Пример 3.10.
Построим с плмощью метода резолюций следующий вывод:
ØA É B, C Ú A, B É ØC ├ A,
Или, что то же:
ØA É B, C Ú A, B É ØC, ØA ├ .
Перепишем все посылки в виде дизъюнктов:
A Ú B, C Ú A, ØB Ú ØC, ØA ├ .
Выпишем по порядку все посылки и начнем их по очереди склеивать по правилу резолюций:
1) A Ú B
2) C Ú A
3) ØB Ú ØC
4) ØA
5) A Ú ØC (1, 3)
6) B (1, 4)
7) A Ú ØB (2, 3)
8) C. (2, 4)
9) A (2, 5)
10) ØC (3, 6)
11) ØB (3, 8)
12) ØC (4, 5)
13) ØB (4, 7)
14) (4, 9)
Мы видим, что такая стратегия перебора неэффективна. В данном случае существует более быстрый вывод. Например:
5) B. (1, 4)
6) C. (2, 4)
7) ØB. (3, 6)
8) . (5, 7)