Лекция 5_3гр

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

2.

3.

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

4.

5.

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

6.

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

7.

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

8.

9.

Рассмотрим множество дизъюнктов полученной КНФ
формулы Ψ :