29. Метод резолюций

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

Для выяснения тождественной истинности или тождественной ложности любой формулы существует 2 основных подхода:

1. Вычислять на всех наборах, что не эффективно в случае большого количества переменных, так как количество вычислений растет в арифметической прогрессии (например, для n переменных число вычислений , при этом вычисления могут быть не только простыми).

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

32. КНФ – конъюнктивная нормальная форма, представляющая собой конъюнкцию дизъюнкций. С целью упрощения, КНФ в методе резолюций будет представляться списком дизъюнктов S.

34. Основная идея метода. Необходимо выяснить является ли данная формула тождественно истинной? Вместо этого решается противоположная задача. Выясняется тождественная ложность отрицания формулы . Обосновывается это тем, что мы работаем с КНФ. Следовательно, если хотя бы одна конъюнкция становится равной нулю, то и вся формула в виде КНФ становится равной нулю.

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

Метод резолюций предлагает более целенаправленное преобразование, позволяющее выяснить тождественную истинность или тождественную ложность формул.

Рассмотрим работу метода резолюций. Допустим, имеется 2 дизъюнкта:

Где - литера;

- некие формулы, представляющие собой некие дизъюнкции.

Тогда, дизъюнкт называется резольвентой дизъюнктов по литере .

Если дизъюнкты не содержат контрарных литер, то резольвенты у них не существует!

Резолютивный вывод – поиск резольвент, представляющий собой в результате последовательность дизъюнктов, принадлежащих к исходному множеству дизъюнктов плюс резольвенты предшествующих дизъюнктов.

Допустим, была некая формула в КНФ:

Заменяем согласно правила резолюций две скобки (дизъюнкты) на , что приводит к упрощению формулы:

Допустим, что мы свели первый дизъюнкт к , а второй дизъюнкт к , то есть получили контрарную пару, что говорит о том, что КНФ равна нулю.

Это же можно доказать применив правило резолюций, добавив к дизъюнктам и пустой дизъюнкт

Применив правило резолюции, получится пустой дизъюнкт #.

Особенно удобен метод резолюций, когда логическая проблема представлена в следующем виде:

Доказать, что из посылок (формул) , следует некоторое следствие В» . Данная задача эквивалентна следующей записи .

Таким образом, задача сводится к выяснению, является ли данная формула тождественно истинной. Как говорилось, метод резолюций вместо выяснения тождественной истинности формулы , выясняет тождественную ложность отрицания данной формулы .