Логическое следование формул

1. Логическое следование формул

2.

Определение. Формула называется
логическим следствием формул 1,..., m , если
при любой подстановке в эти формулы вместо
X 1 ,..., X n
их
переменных
конкретных
A1 ,..., An
высказываний
из
истинности
высказываний 1 ( A1,..., An ),..., m ( A1,..., An ) следует
истинность высказывания ( A1,..., An ) .
Символическое обозначение 1,..., m | называется логическим следованием.
Формулы 1,..., m называются посылками и
формула – следствием логического
следования 1,..., m | .

3.

Определение. Множество формул
называется противоречивым, если из него
логически следует любая (в том числе и
.
тождественно
ложная)
формула
Символически это записывается
.
В противном случае множество формул
называется выполнимым.
Лемма
(Транзитивность
логического
следования). Если 1,..., m | и для любого
значения 1 i m выполняется 1,..., k | i , то
1 ,..., k | .

4.

Лемма (Критерии логического следования).
Условие 1,..., m | равносильно каждому из
следующих условий:
a) 1 ... m | ,
b) | 1 ... m ,
c)
.
В частности, | равносильно | .
Отсюда также следует, что равносильно
тому, что | и | .

5.

Основные правила логического следования:
1) правило отделения (или правило модус
поненс – от латинского modus ponens)
, | ;
2) правило контрапозиции
| ;
3) правило цепного заключения
1 2 , 2 3 | 1 3 ;
4) правило перестановки посылок
1 ( 2 3 ) | 2 ( 1 3 ) .

6.

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

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

8.

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

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

10.

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

11.

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

12.

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

13.

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

14.

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

15.

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

16.

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

17.

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

18.

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

19.

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