5.6. Алгоритм редукции

Алгоритм редукции позволяет доказать общезначимость формул с помощью приведения их к противоречию. Рассмотрим работу алгоритма на примере.

Пример. Проверить общезначимость формулы ((p q) r) (p(qr)).

Предположим, при некоторой интерпретации формула принимает значение F. По таблице истинности импликация принимает значение F тогда и только тогда, когда посылка истинна, а заключение ложно, следовательно, должно выполняться условие: I(p(qr)) = F, а I((pq) r) = T.

Аналогично для следующего шага: I(p)=T, а I(qr)=F.

В результате получаем следующий набор интерпретаций: I(p)=T, I(q)=T, I(r)=F.

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

5.7. Алгебраический подход к определению класса формул

Все изложенные выше алгоритмы реализуют логический подход к определению класса формул, при котором исходная формула не изменяется. Существует другой, алгебраический, подход, при котором формула преобразуется по определенным законам, приводится к нормальной форме, а затем исследуется ее выполнимость.

Для формул исчисления высказываний справедливы следующие законы преобразования:

1. Законы дистрибутивности

((xy)z)((xz)(yz)

((xy)z)((xz)(yz)

2. Закон исключения третьего

(x┐x)T, (x┐x)F

3. Законы де Моргана

┐(xy)( ┐x┐y)

┐(xy)( ┐x┐y)

4. Преобразование импликации

xy(┐xy)

5. Двойное отрицание

┐┐xX

5.7.1. Нормальные формы и алгоритм нормализации

Каждая логическая формула может изучаться алгебраически путем приведения ее к нормальной форме. Возможно приведение к двум нормальным формам – конъюнктивной нормальной форме (КНФ) и дизъюнктивной нормальной форме (ДНФ).

Конъюнктивная нормальная форма – это конъюнкция конечного числа дизъюнкций, т. е. формула вида (L₁L_n) L_i , где L_i – дизъюнкты.

Дизъюнктивная нормальная форма – это дизъюнкция конечного числа конъюнкций, т. е. формула вида (L₁L_n)L_i, где L_i – конъюнкты.

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

Алгоритм нормализации

1. Исключение операций равносильности и импликации:

а) (XY) заменяется на (XY)(YX);

б) (UV) заменяется на (┐U  V).

2. Продвижение знака ┐ до высказываний (по законам де Моргана) и погашения двойных отрицаний.

3. Применение законов дистрибутивности, в результате – получение КНФ или ДНФ.

4. Удаление общезначимых дизъюнктов (дизъюнктов, содержащих р┐р) и повторяющихся литер, в результате – получение приведенной нормальной формы (КНФ или ДНФ).

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

Пример. Привести формулу (p(qr))((ps)r) к КНФ.

1. (p(qr)) ((ps)r);

2. (p( qr)) ((ps)r);

3. ( p( qr)) ((ps)r);

4. ( p( qr)) ( (ps)r);

5. ( p( qr)) ( p sr);

6. ( p qr)( p sr);

7.  ( p qr)( p sr);

8. (pq r)  ( p sr);

9. ((p p)(q p)( r p))( sr);

10. (p p sr)  (q p sr)  (r p sr);

11. (q p sr).

Формула ложна при q=F, r=F, p=T, s=T.

Таким образом, проблема общезначимости КНФ сводится к проверке общезначимости каждого дизъюнкта, более интересна проблема выполнимости.