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

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

1 МАТЕМАТИКА И МАТЕМАТИЧЕСКОЕ МОДЕЛИРОВАНИЕ Т В Карягина Метод резолюций в логике высказываний и предикатов Аннотация: в статье рассмотрен метод резолюций в применении к логике высказываний и логике предикатов Ключевые слова: метод резолюций, логика предикатов, логика высказываний, хорновские дизъюнкты, унификация Подход к определению общезначимости формулы в рамках формальной теории более удобный, чем в рамках логики предикатов В силу неалгоритмичности проблемы разрешимости логики предикатов существуют формулы, для которых неизвестно, как построить их вывод В 1965 г американский математик Дж Робинсон сформулировал еще один подход к этой алгоритмически неразрешимой задаче Он предложил перевести проблему в рамки игры с формулами по более простым правилам, чем правила вывода исчисления предикатов Этот подход был назван методом резолюций Он применяется для установления факта, что некоторая формула логики высказываний является противоречием Сначала рассмотрим метод резолюций в применении к логике высказываний, затем перенесем метод на логику предикатов Определение 1 Атомарную формулу логики высказываний, или ее отрицание, назовем литерой Литеры будем обозначать строчными латинскими буквами Пример 1 Формулы a P, b P являются литерами, а формула P Q не является литерой Определение 2 Конечная дизъюнкция литер или их отрицаний называется дизъюнктом Пустой дизъюнкт обозначается и означает ложь, или тождественно-равную нулю формулу Пример 2 Дизъюнкции: ab, ab, pqr, p являются дизъюнктами, а формула a p q Карягина Татьяна Васильевна, кандидат технических наук, доцент кафедры математики и информатики Российского государственного университета Базовое образование: математический факультет Мордовского государственного университета им Н П Огарева Тема кандидатской диссертации: «Математическое моделирование динамических процессов в кристаллах кремния после лазерного облучения» Основные публикации: «Применение численных методов при построении функции распределения интегральной интенсивности» (2010); «Обработка кривых распределения интегральной интенсивности с помощью преобразования Фурье» (2010); «Математическое моделирование как методология научных исследований» (2010); «Преобразование Фурье и вейвлет-анализ как формы математического моделирования» (2011) Сфера научных интересов: математическое моделирование динамических процессов E-mal: нет Определение 3 Два дизъюнкта называются резольвентной парой, если существует такая литера, которая участвует в одном дизъюнкте как положительная, а в другом как отрицательная Пример 3 Пара дизъюнктов ab, ab c резольвентная, тк литера b участвует в первом дизъюнкте как положительная, а во втором как отрицательная Пара ab, a c не является дизъюнктной парой Теорема 1 Пусть 1, 2 резольвентная пара дизъюнктов вида 1 A p, 2 p, где через A, обозначены члены дизъюнктов с невыделенными литерами Тогда формула A p pa является тавтологией, те тождественно-истинной, или логическим законом Из теоремы следует правило получения из резольвентной пары нового дизъюнкта, который называется резольвентой Это правило называется правилом резолюции, и его записывают в виде A p, p A 37

2 УЧЕНЫЕ ЗАПИСКИ 9 (I), 2012 Это правило по виду напоминает правило mous ponens в формальной теории которое соответствует логическому закону или в виде AA,, A A A A Последняя формула соответствует правилу резолюции A, A Пример 4 Резольвентой для пары ab p, c p будет дизъюнкт ab c Применим правило резолюции к паре pq r, q r Получим резольвенту p r Идея метода резолюций 1 Пусть требуется доказать в алгебре высказываний, что формула F тавтология 2 Рассмотрим отрицание этой формулы G F Тогда задача переформулируется и станет следующей Доказать, что формула G тождественно-ложная 3 Преобразуем формулу G в конъюнктивную нормальную форму (КНФ) G 1 n, где дизъюнкты 4 Среди дизъюнктов найдем резольвентную пару и применим к ней правило резолюции Полученный новый дизъюнкт, резольвенту, обозначим n 1 и добавим в формулу КНФ для G : G 1 n n 1 Тем самым получим новую КНФ для G 5 Если резольвента n 1 является пустым дизъюнктом, то формула G будет тождественной ложью, задача решена Если нет, то найдем среди всех дизъюнктов 1,, n, n 1 резольвентную пару Применим к ней правило резолюции и добавим полученную резольвенту к имеющимся дизъюнктам Будем повторять пункты 4 и 5, пока не получим пустой дизъюнкт Пример 5 Пусть G abacbc a Докажем, что G тождественно-ложная формула, методом резолюций Найдем среди дизъюнктов резольвентную пару Таких пар много, например, 1, 3, 1, 4, 2, 3, 2, 4 Найдем резольвенту для 1, 3 Получим 5 a c Далее, применим правило резолюции для пары 2, 5 Получим новый дизъюнкт 6 a Резольвентой для пары 4, 6 будет 7 На этом решение задачи заканчивается Для удобства применения метода резолюций используют следующую запись 1 a b 2 a c 3 b c 4 a 5 a c для 1, 3 6 a для 2, 5 7 для 4, 6 Теоретическим обоснованием метода резолюций являются теоремы 2 4 Теорема 2 (о резольвентной паре) Пусть формула G тождественно-ложная и представлена в КНФ G 1 n Тогда среди дизъюнктов существует резольвентная пара Теорема 3 (о добавлении резольвенты) Пусть формула G 1 n представлена в КНФ, и среди дизъюнктов существует резольвентная пара Тогда добавление в формулу КНФ резольвенты n 1 этой пары является равносильным преобразованием формулы G, те G 1 n 1 n n 1 38

3 МАТЕМАТИКА И МАТЕМАТИЧЕСКОЕ МОДЕЛИРОВАНИЕ Теорема 4 (о пустой резольвенте) Если формула G тождественно-ложная и представлена в КНФ, то среди всех резольвент исходных дизъюнктов и вновь получаемых дизъюнктов по правилу резолюции существует пустой дизъюнкт Хорновские дизъюнкты Дальнейшим упрощением метода резолюций является идея американского математика Хорна использовать только дизъюнкты определенного вида Определение 4 Дизъюнкт, у которого среди литер не более одной положительной, называется хорновским При этом дизъюнкт с одной положительной литерой и наличием отрицательных литер вида ab c b c a называется правилом и читается так: «из b,, c следует a» Дизъюнкт без положительной литеры вида b c b c называется целевой дизъюнкт и читается так: «из b,, c следует ложь» Дизъюнкт без отрицательных литер только с одной положительной литерой вида a 1 a называется фактом и читается: «справедливо a» Вывод Для того чтобы доказать методом резолюций, что G тождественно-ложная, рекомендуется выполнить ряд действий 1 Привести G к КНФ 2 Преобразовать все дизъюнкты в КНФ в хорновские путем переобозначения некоторых положительных литер в отрицательные 3 Если все дизъюнкты в КНФ хорновские, то применение метода резолюций облегчается тем, что всегда можно вести поиск очередной резольвентной пары при помощи одной из следующих двух рекомендуемых стратегий Стратегия от фактов Если среди хорновских дизъюнктов есть факт, те одиночная положительная литера, то нужно искать второй дизъюнкт, который составляет с ним резольвентную пару После применения правила резолюций к такой паре получается резольвента, которая будет короче второго дизъюнкта При этом если существуют несколько дизъюнктов, парных данному факту, то рекомендуется сначала рассматривать дизъюнкты более короткие Потом снова ищем факт и к нему короткий парный дизъюнкт и тд Получаем множество новых фактов Стратегия от цели Если среди хорновских дизъюнктов есть целевой, те дизъюнкт без положительной литеры, то нужно искать второй дизъюнкт, который с ним составляет резольвентную пару Далее, каждый раз для очередной резольвенты нужно искать парный ей дизъюнкт и применять правило резолюций Получаем дерево подцелей Замечание 1 Так как решаемая задача в общем алгоритмически неразрешимая, то может случиться, что ни одна из предлагаемых стратегий не приведет к успеху Тогда нужно применять правило резолюций по какой-либо третьей стратегии и тд Пример 6 Рассмотрим формулу G (см пример 5) Сделаем замену литеры a на литеру p, чтобы все дизъюнкты в КНФ для G были хорновские: G pbpcbc p Будем доказывать тождественную ложь формулы G методом резолюций, используя стратегию от фактов В таком случае исходный факт один дизъюнкт 4 1 p b 2 p c 3 b c 4 p 5 b для 4, 1 6 c для 4, 2 7 c для 5, 3 8 для 6, 7 Теперь для сравнения для той же задачи используем стратегию от цели Целевой дизъюнкт 3 39

4 УЧЕНЫЕ ЗАПИСКИ 9 (I), p b 2 p c 3 b c 4 p 5 p c для 3, 1 6 p для 5, 2 7 для 6, 4 Замечание 2 Метод резолюций, хорновские дизъюнкты и стратегия от цели положены в основу логического программирования на языке Пролог При этом для хорновских дизъюнктов в Прологе записывают 40 abc a: bc, правило «a, если b, c»; a a : факт «справедливо a»; bc : bc, целевой дизъюнкт При такой записи применение метода резолюций напоминает переписывание формул алгебры с целью их упрощения Например, для примера 6 решение задачи на доказательство ложности формулы G выглядит так: 1 b : p 2 c : p 3 : b, c 4 p : (из 3) b, c (из 1) p, c (из 2) p (из 4) Ø Унификация Метод резолюций в логике предикатов Перенесем метод резолюций в логику предикатов Основная идея принадлежит математику Эрбрану Определение 5 Две литеры l 1 P( x), l 2 P( y) называются унифицируемыми, если существуют такие подстановки свободных переменных, при которых литеры совпадут: y l1 l2 P( a) при x a, y a Пример 7 Две литеры l 1 P( f( x)), l 2 P( y) являются унифицируемыми, тк существует подстановка f( x), такая, что l1 l2 P( f( x)) при y f( x) Правило резолюций в логике предикатов применяется только к резольвентной паре с унифицируемой литерой, присутствующей в одном дизъюнкте как положительная литера и в другом как отрицательная Пример 8 Применим правило резолюции к резольвентной паре Px ( ) Axy (, ), Pa ( ) xz (, ) Тогда будем иметь резольвенту Aa (, y) az (, ) Это записывают следующим образом: 1 Px ( ) Axy (, ) 2 Pa ( ) xz (, ) 3 Aa (, y) az (, ) из 1, 2 при x a Большое неудобство для применения метода резолюций в логике предикатов связано с наличием кванторов Для преодоления этой трудности разработаны два приема Один назван в честь математика Сколема исключение по Сколему всех кванторов существования, другой вынос всех кванторов общности за скобки Определение 6 Пусть имеются формулы с кванторами существования: x P( x), y Q( x, y), x y Q( x, y) и тд Тогда исключение по Сколему кванторов существования проводится следующим образом: x P( x) P( a) ; y Q( x, y) Q( x, f( x)) ; xy Q( x, y) Q( a, f( a)) и тд, где, ( ) a f x неизвестные постоянная и функция, называемые сколемовскими Вывод Метод резолюций состоит в следующем: 1) задача доказать общезначимость формулы F ;

5 МАТЕМАТИКА И МАТЕМАТИЧЕСКОЕ МОДЕЛИРОВАНИЕ 2) перейти к формуле G F и сделать отрицание в ней; 3) исключить все кванторы существования в G ; 4) вынести все кванторы общности за скобки, предварительно переобозначив связанные переменные с целью отличия их от свободных переменных и между собой, получим G xy zh ; 5) представить формулу H в КНФ, те H 12 n, и применить к H метод резолюций с унификацией Пример 9 Построим сколемовскую стандартную форму для формулы x y z u v P( x, y, z, u, v, ) Решение: в префиксе формулы три квантора существования Левее Поэтому первый шаг замена переменной x константой Получим: x нет кванторов всеобщности y z u v P( c1, y, z, u, v, ) Перед приставкой u два квантора существования Поэтому переменную u заменяем на двухместный функциональный символ: y z u v P( c, y, z, u, v, ) y z v P( c1, y, z, f1( y, z), v, ) Перед приставкой три квантора всеобщности Значит, используем трехместный функциональный символ: y z vpc ( 1, yz,, f1( yz, ), v, f2( yzv,, )) Последняя формула и есть сколемовская стандартная форма Пример 10 Построим сколемовскую стандартную форму для формулы xyz(( pxy (, ) qyz (, )) rxyz (,, )) Решение: первый шаг приведение матрицы приведенной формы к КНФ: xyz([ pxy (, ) rxyz (,, )] [ qyz (, ) rxyz (,, )]) Далее убираем первый слева квантор существования: x z([ p( x, f1( x)) r( x, f1( x), z)] [ q( f1( x), z) r( x, f1( x), z)]) Убираем и второй квантор существования: x([ p( x, f1( x)) r( x, f1( x), f2( x))] [ q( f1( x), f2( x)) r( x, f1( x), f2( x))]) Пример 11 Доказать общезначимость формулы логики предикатов: Решение: перейдем к формуле G где ( ) ( ) ( ) ( ) xp( x) R( x) F x P x Q x x Q x R x F и сделаем отрицание в G : G H1H2 H3,, H2 xq( x) R( x) H xpx Rx H1 x P( x) Q( x) 3 ( ) ( ) Сделаем отрицание в H 3 и исключим квантор существования: 1, H3 x Px ( ) Rx ( ) Pa ( ) Ra ( ) Сделаем замену связанной переменной «x» в H 2 на «y», вынесем все кванторы общности в G за скобки и представим H в КНФ: G x y P( x) Q( x) Q( y) R( y) P( a) R( a) Теперь применим метод резолюций с унификацией, используя стратегию от фактов 1 Px ( ) Qx ( ) 41

6 УЧЕНЫЕ ЗАПИСКИ 9 (I), Qy ( ) Ry ( ) 3 Pa ( ) 4 Ra ( ) 5 Qa ( ) из 3, 1 при x a 6 Ra ( ) из 5, 2 при y a 7 из 6, 4 Можно было применить стратегию от цели и запись хорновских дизъюнктов с обратной импликацией 1 Qx: ( ) Px ( ) 2 Ry ( ): Qy ( ) 3 Pa ( ): 4 : Ra ( ) (из 4) Ra ( ) (из 2, y a) Qa ( ) (из 1, x a ) Pa ( ) (из 3) Ø Список литературы 1 Логический подход к искусственному интеллекту: от классической логики к логическому программированию: пер с франц Тейз А, Грибомон П, Луи Д и др М: Мир, с 2 Мендельсон Э Введение в математическую логику Пер с англ М: Наука, с 3 Нильсон Н Принципы искусственного интеллекта Пер с англ М: Радио, с 4 Новиков Ф А Дискретная математика для программистов СПб: Питер, с 5 Соболева Т С, Чечкин А В Дискретная математика М: Издат центр «Академия», с 6 Чень Ч, Ли Р Математическая логика и автоматическое доказательство теорем Пер с англ М: Наука, с 42

📎📎📎📎📎📎📎📎📎📎