Нормальные формы формул алгебры высказываний

1. Нормальные формы формул алгебры высказываний

2.

Отношение равносильности является
отношением эквивалентности на множестве
всех формул FАВ, которое разбивает это
множество
на
классы
эквивалентности
[ ] { FАВ : } , определяемые формулами
FАВ .
Из лемм следует, что для каждой формулы
FАВ можно
указать
равносильные
ей
формулы специального вида, содержащие
только символы логических операций , , .

3.

Определение.
Литерой
называется
пропозициональная переменная X или ее
отрицание X . Для обозначения литеры
используется символ X , где {0,1} и по
1
X
X , X 0 X .
определению
Определение.
Конъюнктом
(соответственно, дизъюнктом) называется
литера или конъюнкция (соответственно,
дизъюнкция) литер.
Конъюнкт
(дизъюнкт)
называется
совершенным,
если
он
содержит
все
пропозициональные
переменные
рассматриваемой формулы.

4.

Определение. Конъюнктивной нормальной
формой (сокращенно КНФ)
называется
дизъюнкт или конъюнкция дизъюнктов.
Дизъюнктивной
нормальной
формой
(сокращенно ДНФ) называется конъюнкт или
дизъюнкция конъюнктов.
При этом КНФ (соответственно, ДНФ)
называется совершенной, если совершенны все
ее дизъюнкты (соответственно, конъюнкты).
Теорема 1. Любая формула равносильна
некоторой ДНФ и некоторой КНФ.

5.

Алгоритм приведения формулы
к ДНФ
(соответственно, к КНФ):
1) выражаем все входящие в формулу
импликации и эквивалентности через конъюнкцию,
дизъюнкцию и отрицание;
2) согласно законам де Моргана все отрицания,
стоящие перед скобками, вносим в эти скобки и
сокращаем все двойные отрицания;
3)
согласно
законам
дистрибутивности
преобразуем формулу так, чтобы все конъюнкции
выполнялись раньше дизъюнкций (соответственно,
чтобы все дизъюнкции выполнялись раньше
конъюнкций).

6.

Теорема
2.
( X 1 ,..., X n )
Любая выполнимая формула
равносильна формуле вида
где
дизъюнкция
берется
по
всем
1,..., n {0,1}n,
упорядоченным наборам
удовлетворяющим условию F 1,..., n 1 .
Такая формула определяется однозначно (с
точностью до порядка членов конъюнкций и
дизъюнкций) и называется совершенной
дизъюнктивной
нормальной
формой
(сокращенно СДНФ) формулы .

7.

Теорема 3. Любая опровержимая формула
( X 1 ,..., X n ) равносильна формуле вида
где конъюнкция берется по всем упорядоченным
1,..., n {0,1}n, удовлетворяющим
наборам
условию F 1,..., n 0 .
Такая формула определяется однозначно (с
точностью до порядка членов конъюнкций и
дизъюнкций)
и
называется
совершенной
конъюнктивной нормальной формой (сокращенно
СКНФ) формулы .

8.

Алгоритм нахождения СДНФ и СКНФ
формулы ( X 1,..., X n ) :
1. Составить истинностную таблицу
формулы и добавить два столбца
«Совершенные конъюнкты» и «Совершенные
дизъюнкты».
2. Если при значениях ( X 1 ) k1,..., ( X n ) kn
значение ( ( X 1 ,..., X n )) формулы равно 1, то
в соответствующей строке таблицы в столбце
«Совершенные
конъюнкты»
записываем
X1k1 X nk n
конъюнкт
и
в
столбце
«Совершенные дизъюнкты» делаем прочерк.
При этом X i1 X i и X i0 X i .

9.

3. Если при значениях ( X 1 ) m1,..., ( X n ) mn
истинностное значение ( ( X 1 ,..., X n )) формулы
равно 0, то в соответствующей строке таблицы в
столбце «Совершенные дизъюнкты» записываем
X11 m1 X n1 mn
дизъюнкт
и
в
столбце
«Совершенные конъюнкты» делаем прочерк.
X1
…
Xn
...
( X 1 ,..., X n )
… … … ...
k1 … k n ...
… … … ...
m1 … mn ...
…
1
…
0
…
…
…
…
...
Совершенные Совершенные
конъюнкты
дизъюнкты
…
…
–
X1k1 X nk n
…
…
–
X11 m1 X n1 mn
…
…

10.

4. СДНФ формулы равна дизъюнкции
полученных
совершенных
конъюнктов:
( X1k1 X nk n ) … .
5. СКНФ формулы равна конъюнкции
полученных
совершенных
дизъюнктов:
( X11 m1 X n1 mn ) … .

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

12.

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

13.

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

14.

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

15.

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

16.

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

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

18.

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

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

20.

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

21.

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

22.

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

23.

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

24.

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

25.

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

26.

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

27.

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

28.

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

29.

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