Методы проверки тождественной истинности формул

1.

Методы проверки
тождественной
истинности формул

2.

Основные методы проверки тождественной
истинности формул:
1. Прямой метод.
2. Алгебраический метод.
3. Алгоритм Квайна.
4. Алгоритм редукции.
5. Метод семантических таблиц.
6. Метод резолюций.

3.

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

4.

5.

6.

7.

Метод
семантических таблиц
в алгебре высказываний

8.

Оценкой
переменных
в
формуле
= (X1,…,Xn) называется отображение
множества { X1,…,Xn } в множество {0,1}.
Обозначения: | и | .
Семантической таблицей
называется
упорядоченная пара множеств формул
| .

9.

Семантическая
таблица
|
называется
выполнимой, если существует такая оценка
переменных , что
1)
для любой формулы
2)
для любой формулы

10.

Примеры.
1. Семантическая таблица
выполнима для оценки (X)=1, (Y)=0;
2. Семантическая таблица
невыполнима.

11.

Основная
теорема
семантических таблиц.
метода
Для любой формулы условие |
выполняется тогда и только тогда, когда
|
семантическая
таблица
невыполнима.

12.

Пример. С помощью семантических
тождественную истинность формулы
таблиц
которая называется законом Пирса.
Табличный вывод семантической таблицы
докажем
:

13.

Метод резолюций в алгебре
высказываний

14.

Следующие задачи равносильны:
а) проверка тождественной истинности
формул;
б) проверка логического следования формул;
в) проверка тождественной ложности формул;
г) проверка противоречивости множества
формул;
д) проверка противоречивости множества
дизъюнктов.

15.

Определение.
Пусть
для
некоторой
переменной X дизъюнкты D1 , D2 представимы в
виде D1 D1 X , D2 D2 X . Тогда дизъюнкт
D1 D2 называется резольвентой дизъюнктов
D1 , D2
по переменной X и обозначается
ResX ( D1 , D2 ) .
Резольвента дизъюнктов D1 , D2 по некоторой
переменной
X
называется
резольвентой
дизъюнктов D1 , D2 и обозначается Res ( D1 , D2 ) .
По определению Res ( X , X ) =0.
Свойство. Если D1 D1 X , D2 D2 X .
выполнимы, то выполнима ResX ( D1 , D2 ) .

16.

Определение. Резолютивным выводом
формулы из множества дизъюнктов
называется
такая
последовательность формул
, что:
1) n= ;
2) каждая из формул i (i=1,…,n) либо
принадлежит
множеству
S,
либо
является резольвентой i Re s( j , k )
предыдущих формул j, k при
некоторых 1 j,k i.

17.

Основная
теорема
метода
резолюций.
Множество
дизъюнктов
противоречиво в том и только том случае, если
существует резолютивный вывод значения 0 из
множества S.
Так как по критерию логического следования
соотношение
F1 ,..., F m |= F
равносильно условию
,
то справедлив следующий результат.

18.

Следствие (Проверка логического следования
формул).
Пусть для формул
формула
имеет
КНФ
.
Тогда логическое следование
равносильно существованию резолютивного
вывода значения 0 из множества дизъюнктов
..

19.

Алгоритм
проверки
следования формул
логического
:
1. Составить формулу
и найти ее КНФ
.
2. Найти резолютивный вывод значения 0
из множества
.
3. Если такой вывод существует, то
выполняется
.

20.

Пример.
Методом
логическое следование:
резолюций
проверим
( X Z ), (Y W ), ((W Z ) V ), V |= X Y .
Данное соотношение равносильно условию
( X Z ), (Y W ), ((W Z ) V ), V , ( X Y ) |=,
т.е. условию противоречивости формулы
= ( X Z ) (Y W ) ((W Z ) V ) V ( X Y ) .

21.

Найдем КНФ этой формулы:
= ( X Z ) ( Y W ) ( (W Z ) V ) V ( X Y ) =
= ( X Z ) ( Y W ) ( W Z V ) V X Y .
Рассмотрим множество дизъюнктов
S = { X Z , Y W , W Z V , V , X ,Y } .
Построим резолютивный вывод значения 0 из
этого множества S:

22.

1 = ResX ( X Z , X ) = Z,
2 = ResY ( Y W ,Y ) = W,
3 = ResZ ( W Z V , Z ) = W V,
4 = ResW ( 2 , 3 ) = V,
5 = Res ( 4 , V ) = 0.
Таким
образом,
множество
дизъюнктов
формулы противоречиво и, значит, выполняется
исходное логическое следование.

23.

Алгоритм
проверки
истинности формулы :
1. Рассмотреть формулу
и найти ее КНФ
тождественной
.
2. Найти резолютивный вывод значения 0
из множества
.
3. Если такой вывод существует, то
выполняется |= .

24.

Задача 2. Методом резолюций
тождественную истинность формулы:
Φ=