матлогика_методичка. Методические указания к выполнению практических работ Омск Издательство Омгту 2009
 Скачать 0.58 Mb.
|
3.2. Автоматическое доказательство теорем. Метод резолюцийПусть имеется множество формул Г = {A1, A2, …, An} и формула B. Автоматическим доказательством теоремы B называют алгоритм, который проверяет вывод A1, A2, …, An⊢B. Выражение читается следующим образом: "Если посылки A1, A2, …, Anистинны, то истинно заключение B". Проблема доказательства в логике состоит в том, чтобы установить, что если истинны формулы A1, A2, …, An, то истинна формула B. Доказательство этого равносильно доказательству общезначимости некоторой формулы. Наиболее эффективно доказательство общезначимости формул осуществляется методом резолюций. Процедура поиска доказательства методом резолюций фактически является процедурой поиска опровержения, т. е. вместо доказательства общезначимости формулы доказывается, что отрицание формулы противоречиво. При изложении метода резолюций обычно употребляется следующая терминология. Литерой называется выражение A или A. Литеры A и A называются контрарными, а множество {A, A} – контрарной парой. Дизъюнкт – это дизъюнкция литер (или элементарная дизъюнкция). Дизъюнкт называется пустым, (обозначается ), если он не содержит литер. Пустой дизъюнкт всегда ложен, так как в нем нет литер, которые могли бы быть истинными при любых наборах переменных. Рассмотрим применение метода резолюций к исчислению высказываний. Правилом резолюции называют следующее правило вывода:  .Правило резолюции можно записать в следующем виде: AB, AC⊢BC. Дизъюнкт BC называется резольвентой дизъюнктов AB и AC по литере A: BC = resA(AB и AC). Если дизъюнкты не содержат контрарных литер, то резольвенты у них не существует. Для дизъюнктов A и A резольвента есть пустой дизъюнкт: resA(A, A) = . Пример 3.4. Пусть F = ABC, G = ABD. Тогда resA(F, G) = BC BD. resB(F, G) = ACAD. resC(F, G) не существует. Метод резолюций соответствует методу доказательства от противного. Условие A1, A2, …, An⊢ B равносильно условию A1, A2,…, An, B⊢ . Алгоритм построения вывода методом резолюций. Шаг 1. Все формулы посылок A1, A2, …, An и формулу отрицания заключения Bпривести к КНФ. Шаг 2. Выписать множество K дизъюнктов всех посылок A1, A2, …, An и отрицания заключения B: K={D1, D2, …, Dn}. Шаг 3. Выполнить анализ пар множества Kправилу: если существуют дизъюнкты Di, Dj, один из которых Di, содержит переменную Ai, а другой Dj –отрицание Ai, то соединить эту пару логической связкой дизъюнкции DiDjи сформировать по правилу резолюции новый дизъюнкт – резольвенту, исключив содержащих контрарные литеры Ai и Ai. Шаг 4. Процесс продолжаем. Если он заканчивается пустым дизъюнктом, то вывод обоснован. Изложенный алгоритм назывется резолютивным выводом из K. Возможны три случая. 1. Среди множества дизъюнктов нет содержащих контрарные литеры. Это означает, что формула B не выводима из множества формул A1, A2, …, An. 2. После очередного применения правила резолюции получен пустой дизъюнкт. Это означает, что формула B выводима из множества формул A1, A2,…, An . 3. Процесс зацикливается, т. е. получаются все новые резольвенты, среди которых нет пустых. Пример 3.5. Применить для примера 3.2 A (B C), AB ⊢ C метод резолюций. Для этого нужно проверить вывод A (B C), AB, C⊢. Алгоритм решения. Шаг 1. Привести к КНФ формулы A(BC), AB, C. A(BC) A(BC) ABC. Формулы AB, C уже находятся в КНФ. Шаг 2. Составим множество К дизъюнктов: К = {A B C, A, B, C}. Шаг 3. Построим резолютивный вывод из K. Выпишем по порядку все дизъюнкты из K:
Вместо пары дизъюнктов, содержащих контрарные литеры запишем их резольвенту (в скобках указаны номера формул, образующих резольвенту):
Вывод заканчивается пустым дизъюнктом, что является обоснованием вывода A (B C), AB ⊢ C. |