Математическая логика и теория алгоритмов

1.6 Методы проверки выводимости формул ИВ

назад | оглавление | вперёд

 

       В этом разделе приводятся некоторые методы проверки тождественной истинности формул ИВ или, как было показано, выводимости формул в ИВ.

        Тривиальный метод заключается в проверке значений формулы при всевозможных значениях (интерпретациях) ее переменных. Однако при большом количестве переменных такой метод становится очень громоздким.

       Алгебраический метод более совершенный. Он базируется на применении законов булевой алгебры. Поскольку разные формулы могут принимать одинаковые значения, то для проверки И можно использовать наиболее простую формулу, например ДНФ (или КНФ), для которых известны методы построения и вычисления значений формулы.

       Метод Куайна представляет собой модификацию тривиального метода. Пусть – множество высказывательных переменных в формуле F . Возьмем первую переменную X 1 и придадим ей, например, значение 1 (или 0). Подставим это значение в формулу F и выполним вычисления, которые могут возникнуть при такой подстановке. После выполнения вычислений получим формулу F ’ с меньшим количеством переменных и применяем к ней описанную процедуру. Если на каком-то шаге получена формула, которая является тавталогией или противоречием независимо от значений высказывательных переменных, входящих в эту формулу, то алгоритм на этом шаге можно остановить. Таким образом, алгоритм Куайна приводит к рассмотрению меньшего количества интерпретаций, чем тривиальный алгоритм. Рассмотрим пример работы метода Куайна.

Пример 1. Проверить выводимость формулы методом Куайна.

  1. Положим X =0. Тогда при любой интерпретации (значении) Y и Z .
  2. Пусть теперь X =1. Тогда . Для полученной формулы повторим процедуру метода Куайна.

       Таким образом, данная формула является тавтoлогией, а значит выводима в ИВ.

Пример 2. Проверить выводимость методом Куайна.
        Сначала применим теорему дедукции к данной выводимости. По теореме дедукции можно проверять выводимость . Далее поступаем как в примере 1.

Пример 3. Проверить выводимость методом Куайна.
       Сначала применим теорему дедукции к данной выводимости. По теореме дедукции можно проверять выводимость .        При Y = Z = 1 получаем,что формула ложна. Таким образом, формула не является тавтoлогией, а значит не выводима.

       Теперь рассмотрим метод редукции распознавания тождественно истинных формул в ИВ. Он особенно удобен, когда в записи формул встречается много импликаций. Суть метода заключается в следующем. Пусть формула F имеет вид импликации, например, . Допустим, что в некоторой интерпретации формула F принимает значение 0. Тогда в соответствии с таблицей истинности для импликации имеем A=1, B=0. Таким образом, проверка формулы F сводится к проверке формул А и В. После этого данный процесс применяется к формулам А и В и т.д.

Пример 4. Проверить выводимость формулы методом редукции.
       Пусть в некоторой интерпретации формула имеет значение 0. Тогда:

       Применим теперь метод редукции к формуле . Если она в некоторой интерпретации имеет значение 0, то:        Для формулы метод редукции дает .
       Из получаем, что . Однако это приводит к противоречию с . Таким образом, исходная формула не может быть ложной ни при какой интерпретации, т.е. формула является тавтoлогией, а следовательно выводима в ИВ.

Пример 5. Проверить выводимость формулы методом редукции.
       По теореме дедукции будем доказывать выводимость . Далее поступаем как в примере 4.

Пример 6. Проверить выводимость формулы методом редукции.
       Сначала применим теорему дедукции к данной выводимости. По теореме дедукции можно проверять выводимость .
       Пусть в некоторой интерпретации формула имеет значение 0. Тогда:        Отсюда и Х=1, Z=1. Tаким образом, существует интерпретация (значения) переменных (X=1,Y=1,Z=1),при которой формула является ложной. Значит формула не выводима в ИВ.

       Наиболее известный классический алгоритм проверки выводимости формул в ИВ называется методом резолюций. В основе метода резолюций положена следующая теорема (доказательство от противного).

Теорема. , где В – любое противоречие, то .
Доказательство. - тавтoлогия. Преобразуем эту формулу.
       . Следовательно, – тавтoлогия, тогда и только тогда, когда .
       Теорема доказана.

        B качестве формулы В при доказательстве от противного по методу резолюций принято использовать пустую формулу, которую будем обозначать . Пустая формула не имеет никакого значения и не является истинной ни при какой интерпретации и, по определению является противоречием.

       Метод резолюций работает с особой стандартной формой формул, которые называются предложениями. Предложение – это дизъюнкция переменных или их отрицаний (литералов). Любая формула исчисления высказываний может быть преобразована во множество предложений следующим образом. Сначала формула приводится к КНФ, а затем конъюнкция дизъюнкций литералов разбивается на множество предложений.

Пример 7. Найдем множество предложений, соответствующих формуле .
       Приведем формулу к КНФ: .
       Таким образом, множество предложений состоит из двух формул и .
       Рассмотрим теперь правило резолюции, т.е. правило вывода, которое используется в методе резолюций. Пусть А и В – два предложения в ИВ и пусть , а , где Р – переменная, а А11 – любые предложения (в частности, может быть пустые или состоящие только из одного литерала). Правило вывода называется правилом резолюции. Предложения А и В называются резольвируемыми (или родительскими), предложение – резольвентой, а формулы контрарными литералами.

Теорема. Правило резолюции логично, т.е. резольвента является логическим следствием резольвируемых предложений.
Доказательство. Пусть I( A )=И и I( B )=И при некоторой интерпретации. Тогда:

       Теорема доказана.

       Пусть нужно установить выводимость . Воспользуемся доказательством от противного и будем доказывать выводимость с помощью метода резолюций . Для этого каждая формула множества Г и формула ¬ F независимо преобразуются в множества предложений. В полученном совокупном множестве предложений отыскиваются резольвируемые предложения, к ним применяется правило резолюции (ПР) и резольвента добавляется во множество до тех пор, пока не будет получено пустое предложение. При этом возможны два случая:


Пример 8. Докажем методом резолюций теорему .
       Преобразуем во множество предложений отрицание целевой формулы:

       .

        Таким образом, множество предложений состоит из . Tеперь производим резольвирование:

  1. X
  2. Y
  3. Z
  4.                   ПР из 2 и 4
  5.                      ПР из 3 и 5
        Поскольку получено пустое предложение, то исходная формула выводима в ИВ.

Пример 9. Докажем методом резолюций выводимость .
       Преобразуем во множество предложений отдельно гипотезу и отдельно отрицание целевой функции. Гипотеза дает предложения . Отрицание целевой формулы дает следующие предложения , поскольку:
       

        Таким образом общее множество предложений . Далее резольвируем как в примере 8.

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

        Tеперь производим резольвирование:

  1. X
  2. Y                  ПР из 1 и 2
  3. Z                  ПР из 1 и 3
       Таким образом, дальнейшее резольвирование невозможно (т.к. нет резольвируемых предложений) и выводимость формулы не доказуема.

Пример 11. Перевести рассуждение в логическую символику и проверить результат на правильность: Он сказал, что придет, если не будет дождя. Но идет дождь. Значит, он не придет.
       Выделим отдельные высказывания и обозначим их.        Рассуждение состоит их двух гипотез:
  1. Он сказал, что придет, если не будет дождя = ;
  2. Но идет дождь = B;
       Вывод из этих гипотез - Значит, он не придет = .
       Таким образом, в логической символике рассуждение выглядит так: .
       Проверим правильность рассуждения методом резолюций.
       Множество предложений, соответствующее двум гипотезам и отрицанию вывода, состоит из следующих предложений . Среди предложений нет резольвируемых, поэтому рассуждение ложное.
назад | оглавление | вперёд