WWW.NET.KNIGI-X.RU
БЕСПЛАТНАЯ  ИНТЕРНЕТ  БИБЛИОТЕКА - Интернет ресурсы
 

«1. Метод Правило резолюции в логике высказываний представляет собой умозаключение со следующей структурой A B, ¬A C BC Здесь A, B и C - произвольные формулы логики высказываний. Высказывание под ...»

Метод резолюции в

Исчислении высказываний

В.Я. Беляев

Лекция

1. Метод

Правило резолюции в логике высказываний представляет собой умозаключение со следующей структурой

A B, ¬A C

BC

Здесь A, B и C - произвольные формулы логики высказываний. Высказывание под чертой является следствием высказываний над чертой.

Нетрудно проверить, что как и полагается для строгого логического

или дедуктивного умозаключения, истинность этого нижнего суждения

с необходимостью следует из истинности верхних посылок.

Метод резолюции заключается в своеобразном способе проверки, выводится или нет данная формула A из множества формул. Далее рассматривается только случай конечного множества. Выражение |= A означает семантическую выводимость формулы A из, т.е. тот факт, что из истинности всех формул обязательно следует истинность A. Согласно теореме о полноте |= A равносильно тому, что A. В лекциях это доказано, когда в записи формул допускаются только две логические связки: ¬ и. Однако подобная теорема может быть доказана для любого полного набора логических связок.

Доказательство выводимости методом резолюции можно делать при любом наборе логических связок, но выводимость при этом понимается скорее как некий алгоритм переработки исходных данных, а не как цепочка умозаключений. Хотя заканчивается он все таки последовательностью применений правила резолюции. Допустим, что нам хочется доказать, что |= A. Для начала замечаем, что выводимость A из равносильна невозможности сделать истинными все формулы множества, ¬A.

Если формулы некого множества нельзя сделать истинными одновременно ни при каких значениях пропозициональных переменных, то такое множество называется противоречивым. Если, наоборот, найдутся такие значения п.п., при которых все формулы истинны, то оно называется выполнимым.

Противоречивость некого множества записывается как |= или. В нашем случае надо доказать, что, ¬A. Пусть далее =, ¬A.

доказательство противоречивости делается в два основных этапа.

Этап 1. Каждую формулу из приводим к конъюнктивной нормальной форме.

Напомним, что конъюнктивная нормальная форма (КНФ) представляет собой конъюнкцию некоторого числа (может быть одного) дизъюнктов. А дизъюнкт - это дизъюнкция некоторого числа (может быть одного) базисных формул, к коим мы относим пропозициональные переменные и отрицания пропозициональных переменных.

Примеры дизъюнктов:

X, ¬X, X Y, X Y ¬Z, X Y X, X Y ¬X, ¬Y Z.

Соответственно примером КНФ может служить формула ¬X&(X Y ¬Z)&(¬Y Z) В дальнейшем вместо ¬A будем писать A и вместо A&B писать A · B или AB. Тогда последний пример КНФ может быть записан как X (X Y Z )(Y Z) Итак, каждая формула из приведена к конъюнктивной нормальной форме. Теперь можно, очевидно, заменить на совокупность всех полученных при этом дизъюнктов. Выполнимость или невыполнимость при этом сохраняется. Поэтому далее можем считать, что состоит из конечного числа дизъюнктов. Наведем в этом множестве небольшой порядок и перейдем к этапу 2. Наведение порядка означает, что мы: a) в каждом дизъюнкте, где какая-нибудь базисная формула встречается более одного раза, будем писать ее только раз. Другими словами дизъюнкты X X заменим на X, а дизъюнкты X X заменим на X. И b), дизъюнкты, в которых встречается одновременно переменная и ее отрицание просто вычеркнем. Они представляют собой тождественно истинные формулы и на выполнимость или противоречивость никак не влияют. Если после этих вычеркиваний ничего не останется, то, естественно, непротиворечиво, и вопрос закрыт. Поэтому далее считаем, что в есть дизъюнкты и ни в одном из них никакая пропозициональная переменная не встречается дважды. Такие дизъюнкты назовем правильными.

Этап 2. Теперь введем во множество дизъюнктов особый - пустой дизъюнкт.

Обозначим его символом. С точки зрения семантики (смысла) он соответствует тождественно ложной формуле. Правило резолюции предполагает, что резольвента может быть и пустым дизъюнктом.

Соответствующее умозаключение имеет вид A, ¬A На втором этапе множество расширяется за счет применения к парам дизъюнктов этого множества правила резолюции и добавления полученной резольвенты к. Опишем подробно, как именно применяется правило резолюции в этом случае. Допустим, что в имеется два дизъюнкта. Один имеет вид X, другой - X Здесь и - дизъюнкты, возможно пустые. X - пропозициональная переменная. При этом, когда мы говорим, что дизъюнкт имеет вид X, то подразумеваем, что X одна из формул этого дизъюнкта и не обязательно первая, а - дизъюнкция всех остальных. То же и для X. Таким образом мы не различаем дизъюнкты, с точностью до перестановки составляющих их базовых формул. Результатом применения резолюции будет дизъюнкт. Но если в этой дизъюнкции встретится переменная и ее отрицание, то, как раньше этот результат вычеркивался из КНФ, так и теперь применение резолюции ничего на дает. В этом случае мы попросту считаем, что резолюция не применима. Если этого не происходит, но в некоторые базисные формулы встречаются по два или более раз, то пишем их только один раз. Таким образом в случае, когда резолюция применима к двум дизъюнктам, результатом всегда будет правильный дизъюнкт.

Применяя к парам элементов из везде, где это возможно, правило резолюции и добавляя полученные дизъюнкты к, мы в конце концов:

- либо получим пустой дизъюнкт;

- либо придем к ситуации, когда ни одного нового дизъюнкта получить невозможно.

На этом второй этап завершается. В первом случае противоречиво и A. Во втором случае не противоречиво и выводимость места не имеет.

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

По ДНФ сразу будет видно, выполнима она или нет.

Если указанную процедуру легко сделать, то так и надо поступить.

Однако в обычной ситуации, связанной с применением логики к решению какой-то практической задачи, условие задачи описывается достаточно обширным множеством сравнительно простых формул. Их конъюнкция - также сравнительно небольшая формула. Однако попытка ее приведения к ДНФ требует перемножения скобок, а для этого может понадобиться экспоненциальное время. Ведь длина ДНФ имеет в общем случае порядок 2n, где n - длина исходной конъюнкции. Такой алгоритм считается неэффективным.

Применяя метод резолюции мы приводим к КНФ сравнительно короткие формулы и поэтому этап 1 как правило эффективен. Замечательной особенностью метода является то, что и этап 2 для многих задач делается быстро и его легко программировать. Хотя, надо признаться, в общем случае и метод резолюции требует экспоненциальных затрат времени.

Поиск алгоритма, который за полиномиальное время в зависимости от длины КНФ на входе дает ответ выполнима она или нет одна из великих задач в современной дискретной математике. Ее положительное решение было бы революционным прорывом для множества прикладных проблем.

–  –  –

Так как получен дизъюнкт, выводимость доказана.

2. Обоснование Мы уже знаем, что выводимость A равносильна противоречивости, ¬A. Если после приведения формул этого множества к КНФ и последующей серии применений правила резолюции получится пустой дизъюнкт, то, ¬A, очевидно, невыполнимо. Доказательства требует обратное утверждение - если множество дизъюнктов невыполнимо, то из него серией резолюций обязательно выводится пустой дизъюнкт.

До конца параграфа будем использовать значок как символ выводимости дизъюнкта из множества дизъюнктов с помощью серии применений правила резолюции. Выводом дизъюнкта из называем конечную последовательность дизъюнктов 1, 2,..., n в которой n = и каждая i либо из, либо получается из двух предыдущих дизъюнктов этой последовательности с помощью правила резолюции. Само собой разумеется, что все дизъюнкты в этих определениях правильные.

Запись означает существование вывода из.

Лемма 2. Пусть - конечное множество дизъюнктов, - один из дизъюнктов и A - произвольная базисная формула (переменная или отрицание переменной).

Тогда если из, A, то дизъюнкт можно представить как

–  –  –

лемму.

Вывод 3. Если из нельзя вывести пустой дизъюнкт,, A базисная, то и из, A нельзя вывести пустой дизъюнкт.

Доказательство. По лемме 1 часть выводимого из, A должна выводиться из. Но частью пустого дизъюнкта может быть только пустой дизъюнкт. Значит, если, A, то.

Если дополнительно к правилу резолюции использовать правило вывода (назовем его ИЛИ-правило) где, - произвольные дизъюнкты, то множество выводимых из данного дизъюнктов вообще говоря увеличится. Будем писать, что, если существует вывод дизъюнкта из этого, использующий резолюцию и ИЛИ-правило. Понятно, что применение ИЛИ-правила, как и правила резолюции, мы ограничиваем случаями, когда в результате получается правильный дизъюнкт. Другими словами, в не должно быть противоположных базисных формул. Если же какая-то базисная формула встречается дважды, то она просто записывается только один раз.

Вывод 4. Если, то.

Доказательство. Допустим, что не верно. В силу вывода 3 мы можем добавлять к сколько угодно дизъюнктов A для и базисных A. Пустой дизъюнкт выводиться все равно не будет. Если, далее, расширить, присоединяя следствия по правилу резолюции, а затем снова добавлять A и т.д., то все равно не выведется. Это все равносильно построению вывода с применением резолюции и ИЛИправила.

Для множества дизъюнктов и базисной формулы A обозначим теперь через A множество всех дизъюнктов вида A, где.

Как обычно, если A - один из членов дизъюнкции, то A и - одно и то же. А если один из членов дизъюнкции противоположен A, то тождественно истинная формула A в A не заносится.

Лемма 5. Пусть.

Пусть A - любая базисная формула. Допустим, что A - правильный дизъюнкт. Тогда A A Доказательство. Пусть

–  –  –

Лемма 6. Пусть - множество дизъюнктов, X - пропозизиональная переменная.

Тогда если, X и, X, то.

Доказательство. Пусть, X и, X. По лемме 5 отсюда X X и X X. Очевидно, что из только с помощью ИЛИправила выводятся как формулы X, так и формулы X. Значит X и X. Отсюда очевидно, что и в силу вывода 4.

Лемма доказана.

Теперь мы можем доказать основную теорему.

Теорема 7. (Теорема о полноте метода резолюций). Пусть - конечное множество дизъюнктов. Тогда следующие условия равносильны:

a) |=;

b).

Доказательство. То, что из следует |= очевидно из того, что резолюция, как и полагается дедуктивному умозаключению, сохраняет истинность.

Допустим теперь, что не верно и докажем выполнимость. Составим список всех п.п. переменных, которые участвуют в записи формул из. Пусть это X1, X2,..., Xn. Будем расширять, добавляя к нему для каждой Xi либо Xi, либо Xi. При этом будем сохранять условие: «Из нельзя вывести ». Сделать это возможно в силу леммы 6. В результате в для каждой Xi будет входить либо Xi, либо Xi.

Припишем теперь всем Xi значения истинности по следующему правилу:

{ 1, если Xi Xi = 0, если Xi Докажем, что при этих значениях все формулы из будут истинны.

Действительно, пусть и ложная формула. Тогда ложны все компоненты дизъюнкта. Допустим, к примеру, что = X 1. Т.к.

X ложен, то X. Правило резолюции позволяет отсюда вывести 1.

Если 1 не пусто, к примеру 1 = Y 2, то Y ложно. Значит Y истинно и Y. Правило резолюции теперь позволит вывести 2. Продолжая, выведем из пустой дизъюнкт и получим противоречие. Таким образом выполнимо и теорема доказана.

–  –  –



Похожие работы:

«Инструкция по эксплуатации приложения "Карта общественных услуг города Таллинна" Содержание Инструкция по эксплуатации приложения "Карта общественных услуг города Таллинна". 1 Введение Главное меню и панель инс...»

«ООО "Меланти" 216790, Россия, г. Рудня, Смоленская обл., ул. Киреева, 79 Огнетушитель порошковый передвижной закачной ОП-35(з), ОП-70(з) ПАСПОРТ РЭ 4854-003-61425156ПАСПОРТ РЭ 4854-003-61425156-2010 на о...»

«Министерство природных ресурсов Российской Федерации Федеральное агентство по недропользованию Российской Федерации Закрытое акционерное общество Горногеологическая компания "МИРЕКО"ГОСУДАРСТВЕННАЯ ГЕОЛОГИЧЕСКАЯ КАРТА РОССИЙСКОЙ ФЕДЕРАЦИИ МАСШТАБА 1:200000 Издание второе Серия Полярно-Уральская Лист Q-41-ХI (Еле...»

«Записки отдела нумизматики и торевтики Одесского археологического музея. II. 2014. С. 59-73. О.Н. Мельников Коммеморативность и соправительство в нумизматике Боспора этапа поздней империи (210-341/342 гг.). Отсутствует общепризнанная гипотеза, объясняющая все доказанные и предполагаемы...»

«2 Форма и содержание вступительного испытания Творческое испытание проводится в форме прослушивания и включает два этапа, в соответствии с которыми абитуриенту необходимо исполнить: два разнохарактерных произведений композиторов 18-20 веков, разнообразных по стилю, форме, жанру, разноплановых по...»

«ИЗЪ МУЗЫКАЛЬНАГО ДНЕВНИКА. 1. Ч’ Ьмъ выше исполнитель. ч%мъ дальше онъ отходить отъ обоихъ мыслимыхъ полюсовъ исполнительства, то-есть т о л ь к о виртуоза и т о л ь к о интерпрета (разумеет...»

«ОРГАНИЗАЦИЯ EP ОБЪЕДИНЕННЫХ НАЦИЙ UNEP/OzL.Pro.WG.1/resumed.38/2 Distr.: General 25 August 2016 Russian Программа Организации Original: English Объединенных Наций по окружающей с...»

«О некоторых проблемах рассмотрения заявлений об обжаловании решений о приостановлении осуществления государственного кадастрового учета (к вопросу о создании апелляционных комиссий) Вступившим в зако...»

«Виды ПО ПО Прикладное Системное Утилиты ОС Библиотеки Трансляторы Демоны Структура ПО Прикладное ПО Системное ПО ОС АППАРАТУРА Функции ОС запуск и исполнение программ управление памятью работа с периферийными устройствами программный интерфейса параллельное выполнение программ организация взаимодействия п...»

















 
2017 www.ne.knigi-x.ru - «Бесплатная электронная библиотека - электронные матриалы»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.