Математическая логика и теория алгоритмов
|
1.6 Методы проверки выводимости формул ИВ |
назад | оглавление | вперёд |
       В этом разделе приводятся некоторые методы проверки тождественной истинности формул ИВ или, как было показано, выводимости формул в ИВ.
        Тривиальный метод заключается в проверке значений формулы при всевозможных значениях (интерпретациях) ее переменных. Однако при большом количестве переменных такой метод становится очень громоздким.
       Алгебраический метод более совершенный. Он базируется на применении законов булевой алгебры. Поскольку разные формулы могут принимать одинаковые значения, то для проверки И можно использовать наиболее простую формулу, например ДНФ (или КНФ), для которых известны методы построения и вычисления значений формулы.
       Метод Куайна представляет собой модификацию тривиального метода.
Пусть –
множество высказывательных переменных в формуле F .
Возьмем первую переменную X 1
и придадим ей, например, значение 1 (или 0). Подставим это значение
в формулу F и выполним вычисления, которые могут возникнуть при такой подстановке. После выполнения вычислений
получим формулу F ’ с меньшим количеством переменных и применяем к ней описанную процедуру. Если на
каком-то шаге получена формула, которая является тавталогией или противоречием независимо от значений высказывательных переменных,
входящих в эту формулу, то алгоритм на этом шаге можно остановить. Таким образом, алгоритм Куайна приводит к рассмотрению меньшего
количества интерпретаций, чем тривиальный алгоритм. Рассмотрим пример работы метода Куайна.
Пример 1. Проверить
выводимость формулы методом Куайна.
       Теперь рассмотрим метод редукции распознавания тождественно истинных формул в ИВ. Он особенно удобен, когда в записи формул встречается много импликаций. Суть метода заключается в следующем. Пусть формула F имеет вид импликации, например, .
Допустим, что в некоторой интерпретации формула F
принимает значение 0. Тогда в соответствии с таблицей истинности для импликации имеем A=1, B=0. Таким
образом, проверка формулы F сводится
к проверке формул А и В. После этого данный процесс
применяется к формулам А и В и т.д.
Пример 4. Проверить выводимость формулы методом редукции.
       Пусть в некоторой интерпретации формула имеет значение 0. Тогда:
       Наиболее
известный классический алгоритм проверки выводимости формул в ИВ
называется методом резолюций. В основе метода резолюций
положена следующая теорема (доказательство от противного).
Теорема. , где В – любое противоречие, то
.
Доказательство. - тавтoлогия. Преобразуем эту формулу.
       .
Следовательно,
–
тавтoлогия, тогда и только тогда, когда
.
       Теорема доказана.
        B качестве формулы В при доказательстве от противного по методу
резолюций принято использовать пустую формулу, которую будем
обозначать . Пустая формула не имеет никакого значения и не является истинной ни при какой
интерпретации и, по определению является противоречием.
       Метод
резолюций работает с особой стандартной формой формул, которые
называются предложениями. Предложение – это дизъюнкция
переменных или их отрицаний (литералов). Любая формула исчисления
высказываний может быть преобразована во множество предложений
следующим образом. Сначала формула приводится к КНФ, а затем
конъюнкция дизъюнкций литералов разбивается на множество предложений.
Пример 7. Найдем множество
предложений, соответствующих формуле .
       Приведем формулу к КНФ: .
       Таким образом, множество предложений
состоит из двух формул и
.
       Рассмотрим теперь правило резолюции, т.е. правило вывода, которое используется в методе резолюций. Пусть А и В –
два предложения в ИВ и пусть , а
, где Р – переменная, а А1,В1 – любые предложения (в частности, может быть
пустые или состоящие только из одного литерала). Правило вывода
называется правилом резолюции. Предложения А и В
называются резольвируемыми (или родительскими), предложение
– резольвентой, а формулы
– контрарными литералами.
Теорема. Правило резолюции
логично, т.е. резольвента является логическим следствием резольвируемых предложений.
Доказательство. Пусть I( A )=И
и I( B )=И
при некоторой интерпретации. Тогда:
       Пусть
нужно установить выводимость .
Воспользуемся доказательством от противного и будем доказывать
выводимость
с помощью
метода резолюций . Для
этого каждая формула множества Г и формула ¬ F
независимо преобразуются в множества предложений. В полученном
совокупном множестве предложений отыскиваются резольвируемые
предложения, к ним применяется правило резолюции (ПР) и резольвента
добавляется во множество до тех пор, пока не будет получено пустое
предложение. При этом возможны два случая:
       .
        Таким образом, множество предложений
состоит из .
Tеперь производим резольвирование:
        Таким образом общее множество
предложений . Далее резольвируем как в примере 8.
Пример 10. Проверим методом резолюций выводимость .
       Применим к выводимости теорему дедукции. Получим
. Еще раз применим теорему дедукции.
Это дает
.
       Преобразуем к множеству предложений
гипотезы и отрицание целевой формулы. Таким образом, получим
предложения .
        Tеперь производим резольвирование: