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

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

2.

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

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

4.

Определение.
Пусть
для
некоторой
переменной 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 ) .

5.

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

6.

Теорема.
Множество
дизъюнктов
S {D1 , , Dm } противоречиво в том и только том
случае, если существует резолютивный вывод
значения 0 из множества S.
Так как по критерию
следования соотношение
логического
1 , , n |=
равносильно условию
1 , , n , |=,
то справедлив следующий результат.

7.

Следствие (Проверка логического следования
формул).
Пусть для формул 1 , , n , формула
1 n
D1 Dm .
имеет
КНФ
Тогда логическое следование 1 , , n |=
равносильно существованию резолютивного
вывода значения 0 из множества дизъюнктов
S {D1 , , Dm } .

8.

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

9.

Пример.
Методом
логическое следование:
резолюций
проверим
( 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 ) .

10.

Найдем КНФ этой формулы:
= ( 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:

11.

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.
Таким
образом,
множество
дизъюнктов
формулы противоречиво и, значит, выполняется
исходное логическое следование.

12.

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

13. Решение логических задач

14.

Задача. Методом резолюций проверьте
справедливость следующих рассуждений.
Допустим, что если руководство вуза
действует по закону высшей школы, то
студент-задолжник не отчисляется, если он
является задолжником не более одного
месяца
или
преподаватель-экзаменатор
уходит в отпуск. Не будет ли отчислен
студент-задолжник, если руководство вуза
действует по закону высшей школы и сессия
только что закончилась?

15.

Решение.
Введем
обозначения
для
следующих высказываний:
D = «руководство вуза действует по закону
высшей школы»;
S = «студент-задолжник отчисляется»;
P = «преподаватель-экзаменатор уходит в
отпуск»;
T = «студент является задолжником не более
одного месяца».
Первое утверждение задачи

16.

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

17.

Рассмотрим множество дизъюнктов полученной
КНФ формулы
и построим резолютивный вывод значения 0 из
этого множества S.