Зарипова, Э.Р. Дискретная математика Часть II. Математическая логика

70 ( ) ( ) { ( )} { ( )} { ( ), ( )} ({ ( ), ( )} { ( )}) ({ ( ), ( )} { ( )}) ) ) ( ( Q a R y Q a R y Q a R y P a Q a P a P a R y P a C L C L 2 2 1 1                  Таким образом Q(a)  R(y) – бинарная резольвента C 1 и C 2 и P(x) и ( ) P a – отрезаемые литеры. Определение. Резольвентой дизъюнктов C 1 и C 2 является одна из следующих резольвент: 1) бинарная резольвента C 1 и C 2 ; 2) бинарная резольвента C 1 и склейки C 2 ; 3) бинарная резольвента склейки C 1 и C 2 ; 4) бинарная резольвента склейки C 1 и склейки C 2 . Пример 14.3. Пусть С 1 =P(x)  P(f(y))  R(g(y)) и     2 ( ) ( ) C P f g a Q b   . Склейка C 1 есть C 1  =P(f(y))  R(g(y)) . Бинарная резольвента C 1  и C 2 есть R(g(g(a)))  Q(b) и она же есть и резольвента C 1 и C 2 . Метод резолюций есть правило вывода, которое порождает резольвенты для множества дизъюнктов. Метод резолюций полон, что доказывается следующей теоремой. Теорема. Множество S дизъюнктов невыполнимо тогда и только тогда, когда существует вывод пустого дизъюнкта П из S (без доказательства). Пример14.4. Применение метода резолюций в исчислении предикатов. Доказать справедливость следующих рассуждений. У всякого шутника из города Габрово найдется шутка о каком-нибудь габровце и его теще, способная рассмешить всех жителей этого города, за исключением тещи габровца. Богдан – большой шутник. У мадам Петковой нет зятя.