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

1.

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

2.

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

3.

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

4.

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

5.

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

6.

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

7.

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

8.

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

9.

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

10.

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

11.

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

12.

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

13.

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

14.

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

15.

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

16.

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

17.

Таким образом, из множества формул S
резолютивно выводится значение 0 и по основной
теореме множество S противоречиво. Следовательно,
формула противоречива и выполняется исходное
логическое следование
, т.е. студентзадолжник не будет отчислен, если руководство вуза
действует по закону высшей школы и сессия только
что закончилась.

18.

Алгебра логических
значений

19.

Пример алгебры дает множество {0,1}
истинностных значений высказываний с nарными операциями F , которые являются
функциями истинностных значений формул
X 1 ,..., X n ,
логики
высказываний
образованных с помощью n пропозициональных
переменных X 1 ,..., X n .
X
Формула
определяет
унарную
операцию F F X (x) , которая обозначается
символом x и называется отрицанием или
дополнением переменной x .

20.

Формулы X Y , X Y определяют
бинарные операции F FX Y ( x, y) , F FX Y ( x, y ) ,
которые обозначаются соответственно символами
x y,x y
и называются дизъюнкцией и
конъюнкцией переменных x ,y.
Операция x y иногда называется также
объединением или суммой переменных x ,y и
обозначается соответственно через x y или
x y.
Операция x y иногда называется также
пересечением или произведением переменных x ,y
и обозначается соответственно через x y или
x y.

21.

Алгебра B=({0,1}, , , ) впервые была введена
в 19-ом веке английским математиком Дж.Булем с
целью применения в логике математических
методов.
Поэтому эта алгебра называется алгеброй Буля
или алгеброй логических значений.

22.

Теорема.
Алгебра
Буля
B=({0,1}, , , )
удовлетворяет свойствам:
1) a (b c) (a b) c , a (b c) (a b) c –
ассоциативность дизъюнкции и конъюнкции;
2) a b b a , a b b a – коммутативность
дизъюнкции и конъюнкции;
a a a
3) a a a ,
–
идемпотентность
дизъюнкции и конъюнкции;
4) a (b c) (a b) (a c) , a (b c) (a b) (a c)
– дистрибутивность соответственно конъюнкции
относительно
дизъюнкции
и
дизъюнкции
относительно конъюнкции;

23.

5) (a ) a – идемпотентность дополнения;
6) (a b) a b , (a b) a b – законы де
Моргана;
a (a b) a
7) a (a b) a ,
–
законы
поглощения;
8) a a 1 , a a 0
– характеристическое
свойство дополнения,
a 1 a
9) a 1 1 ,
– характеристическое
свойство наибольшего элемента 1,
10) a 0 a , a 0 0 – характеристическое
свойство наименьшего элемента 0.

24.

Булевы многочлены и
булевы функции

25.

Для описания алгебраических свойств булевых
алгебр
используются
формулы,
которые
называются булевыми многочленами и которые
образованы
из
булевых
переменных
x,y,…(принимающих значения 0,1) и символов
булевых операций +, , по следующим правилам:
1)
все булевы переменные x,y,… и символы 0,1
– булевы многочлены;
2)
если p и q – булевы многочлены, то
таковыми являются выражения
p q , p q , p .

26.

Если p образован с помощью x1 ,..., xn , то он
обозначается p( x1,..., xn ) .
Множество всех булевых многочленов от n
переменных обозначим Pn .
Если в p( x1,..., xn ) вместо переменных x1 ,..., xn
подставить произвольные значения a1 ,..., an из
множества B, то в результате вычислений
получится некоторый элемент p(a1,..., an ) алгебры B.
Каждый булев многочлен p( x1,..., xn ) определяет
отображение p : Bn B , которое называется булевой
полиномиальной функцией, определяемой булевым
многочленом p( x1,..., xn ) .

27.

p, q Pn
Определение. Булевы многочлены
называются
эквивалентными,
если
они
определяют одну и ту же булеву полиномиальную
функцию, т.е. p q .
Символическая запись: p ~ q или просто p q .
Бинарное
отношение
~
является
эквивалентностью на множестве Pn .
Классы эквивалентности p {q Pn : p ~ q} ,
образуют фактор-множество Pn / ~ { p : p Pn } .
Полные системы представителей этого фактормножества называются системами нормальных
форм булевых многочленов.

28.

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

29.

Дизъюнкт или конъюнкция (совершенных)
дизъюнктов
называется
(совершенной)
конъюнктивной нормальной формой. Сокращенно
КНФ и СКНФ, соответственно.
Конъюнкт или дизъюнкция (совершенных)
конъюнктов
называется
(совершенной)
дизъюнктивной нормальной формой. Сокращенно
ДНФ и СДНФ, соответственно.

30.

Теорема. Любая булева функция f:Bn B
является булевой полиномиальной функцией
следующих булевых многочленов:
pf
f 1,..., n x1
1
1 ,..., n B n
n
...xn
и
qf
( f 1,..., n x1
1
1 ,..., n B
n
n
... xn )
.

31.

Следствие 1. Если булева функция f:Bn B не
равна тождественно нулю, то она является
булевой полиномиальной функцией следующей
совершенной дизъюнктивной нормальной формы
pf
1
n
x1 ...xn
1 ,..., n B n ,
f 1 ,..., n 1
,
которая называется совершенной дизъюнктивной
нормальной формой (сокращенно СДНФ)
функции f .

32.

Следствие 2. Если булева функция f:Bn B не
равна тождественно единице, то она является
булевой полиномиальной функцией следующей
совершенной конъюнктивной нормальной формы
qf
1
( x1 ... x n n )
1 ,..., n B n ,
f 1 ,..., n 0
,
которая называется совершенной конъюнктивной
нормальной
формой
(сокращенно
СКНФ)
функции f .

33.

Алгоритм нахождения СДНФ и СКНФ функции
f:Bn B:
1. Составить таблицу значений функции f и
добавить к ней два дополнительных столбца с
заголовками «Совершенные конъюнкты» и
«Совершенные дизъюнкты».
2. Если при значениях x1 k1,..., xn kn значение
функции f равно 1, то в соответствующей строке
таблицы в столбце «Совершенные конъюнкты»
k1
x1 ...xnk n
записать
конъюнкт
и в столбце
«Совершенные дизъюнкты» сделать прочерк (при
1
0
x
x
x
x ).
этом
и

34.

3. Если при значениях x1 m1,..., xn mn значение
функции f равно 0, то в соответствующей строке таблицы
в столбце «Совершенные дизъюнкты» записать
дизъюнкт x1m1 ... xnmn и в столбце «Совершенные
конъюнкты» сделать прочерк.
x1
…
xn
...
f x1 ,..., xn
…
…
…
…
…
…
…
...
...
...
...
...
…
1
…
0
…
k1
…
m1
…
kn
…
mn
…
Совершенные Совершенные
конъюнкты
дизъюнкты
…
…
–
x1k1 ...xnk n
…
–
…
x1m1 ... xnmn
…
…

35.

4. Дизъюнкция полученных совершенных
конъюнктов
k1
kn
x1 ...xn
+…
является СДНФ функции f , конъюнкция
полученных совершенных дизъюнктов
( x1m1 ... xnmn ) ...
является СКНФ функции f .