Добавил:
Upload Опубликованный материал нарушает ваши авторские права? Сообщите нам.
Вуз: Предмет: Файл:
Скачиваний:
76
Добавлен:
09.02.2015
Размер:
26.29 Кб
Скачать

Лекция 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 и – это замена такая, что

Резольвента для дизъюнктов ищется с помощью унификации термов :

Соседние файлы в папке Мат. логика все лекции