Мат. логика все лекции / Lekcija_5
.docxЛекция 5 Метод резолюций
Метод резолюций в логике высказываний
Предположим, что дана формула логики высказываний А. Для проверки общезначимости формулы А применяют метода резолюций Дж. Робинсона.
Очевидно, что А общезначима тогда и только тогда, когда является противоречием формула ¬A.
Формулу ¬A приводим к конъюнктивной нормальной форме (КНФ):
¬A = ,
где есть дизъюнкция конечного числа переменных или их отрицаний. Тем самым формируется множество дизъюнктов.
Два дизъюнкта этого множества и , содержащие переменные с противоположными знаками, – контрарные литералы, т.е., к примеру, Y и ¬Y, и, следовательно, = , = формируют третий дизъюнкт – резольвенту , в которой исключены контрарные литералы:
.
В частности, если , то резольвента для них – это дизъюнкция, ничего не содержащая (отсутствуют ). Ее называют пустой резольвентой и обозначают знаком □.
Теорема 5.1. Резольвента – это логическое следствие дизъюнктов , т.е.
.
Неоднократно применяя правило получения резольвент к множеству дизъюнкт, стремятся получить пустой дизъюнкт □.
Наличие пустого дизъюнкта □ свидетельствует о получении противоречия, поскольку пустая резольвента получается из двух противоречащих друг другу дизъюнктов Y и ¬Y, каждый из которых логическое следствие формулы ¬A в соответствии с правилом
Получение противоречия с помощью формулы ¬A, означает общезначимость формулы А.
Алгоритм метода резолюций.
Шаг 1. Принять отрицание формулы А, т.е. ¬A.
Шаг 2. Привести формулу ¬A к КНФ.
Шаг 3. Выписать множество ее дизъюнктов:
K = {,...,}.
Шаг 4. Выполнить анализ пар множества К по правилу: если существуют дизъюнкты , один из которых () содержит литерал X, а другой () контрарный литерал ¬X, то нужно соединить эту пару логической связкой дизъюнкции () и сформировать новый дизъюнкт – резольвенту, исключив контрарные литералы X и ¬X.
Шаг 5. Если в результате соединения дизъюнктов, содержащих контрарные литералы, будет получена пустая резольвента – □, то результат достигнут (доказательство подтвердило противоречие), в противном случае включить резольвенту в множество дизъюнктов К и перейти к шагу 4.
При реализации указанного алгоритма возможны три случая:
• Среди текущего множества дизъюнктов нет резольвируемых. Это означает, что формула А не является общезначимой.
• На каком-то шаге получается пустая резольвента. Формула А общезначима.
• Процесс не останавливается, т.е. множество дизъюнкт пополняется все новыми резольвентами, среди которых нет пустых. В таком случае нельзя ничего сказать об общезначимости формулы А.
Метод резолюций пригоден и для доказательства того, что формула B является логическим следствием формул , поскольку,
.
Для того чтобы «запустить» алгоритм метода резолюций, нужно воспользоваться тождеством
Следовательно, формула общезначима, если формула является противоречием. Далее применяем описанный по шагам метод резолюций к формуле А.
Метод резолюций в логике предикатов
Пусть дана формула А. Для проверки общезначимости этой формулы в логике предикатов также применяют метод резолюций, но с некоторыми дополнениями.
Если формула А не содержит предикатов и знаков операций (функций), то фактически имеем формулу исчисления высказываний, поскольку предикаты можно рассматривать как переменные. Следовательно, метод резолюций не требует существенных изменений.
В случае, если формула А содержит кванторы, то ее надо привести к предваренной нормальной форме, а затем выполнить сколемизацию. При этом появятся знаки операций (функций). Затем полученную формулу приводят к конъюнктивной нормальной форме и ищут резольвенты для дизъюнктов.
Возможна ситуация, когда два контрарных литерала, в данном случае они имеют вид содержат два разных терма. Например, . В этом случае проводят их унификацию, т.е. замену термов. Символически унификация записывается в виде
Это означает замену в формуле A терма на терм .
В нашем примере унификация имеет вид:
Далее ищется резольвента:
Сформулируем более строго правила замены термов и понятие унификации.
Определение 5.1. Замена – это пара вида <x | t>, где x – переменная, а t – терм. Применение замены <x | t> к терму t0, входящему в некоторую формулу, определяется индуктивно:
-
x <x | t> = t, если x – переменная;
-
a<x | t>= a, если a – константа;
-
=
Определение 5.2. Унификация двух последовательностей термов t1,…, tn и – это замена такая, что
Резольвента для дизъюнктов ищется с помощью унификации термов :