Дискретная математика (998286), страница 23
Текст из файла (страница 23)
2. Протаскивание отприцаний. Преобразования: ч'х А =ь Вх Х, . Эх А =ь =ьЧх-А, А~А, (Ач'В) =Ь-АЙ-В, (АЙВ) =ь-АЧ-В. После второго этапа формула содержит отрицания только перед атомами. 3. Разделение связанных пврвмвннап. Преобразование: Ятх А(...(~зх В(...х...)...) =ь Я,х А(...92у В(...у...)...), где Ят и Ч2 — любые кванторы. После, третьего этапа формула не содержит случайно совпадающих связанных переменных. 4.
Приведение к првдварвнной форме. Преобразования: Ях А чВ=аьгх (А'~В), Ях АЙВ ~ гвх (АЙВ), где ч — любой квантор. После четвертого этапа формула находится в предваренной форме. 5. Элиминация кванторов существования (сколвмизация). Преобразования: ЗХт СггХ2 (ВьХ„А(ХМХ2...,Хь) =Ь гезХ2 ..-.
Сг„Х„А(а, Х2,...,Х„), 'ч'хт ...'тгхг т Зх, Яг+тхгет...<,>„х„А(хм...,х;,...,х„) =~ =ь Чхт ...'чхг Щььт хг+т...Я„х„А(хт,...,Дхт,...,хг т),...,х„), где а — новая предметная константа, У вЂ” новый функтор, а ьгм г,гг,..., ߄— любые кванторы. После пятого этапа формула содержит только кванторы всеобщности. 6. Элииинацил кванторов всеобщности.
Преобразование: ч'х А(х) =ь А(х). После шестого этапа формула не содержит кванторов. 7. Приведение к конаюнктивной нормальной форме. Преобразование: Ач'(ВЙС) =2 (АчВ)Й(АтгС), (АЙВ)тгС=Ь (АчС)Й(Втг'С). После седьмого этапа формула находится в коньюнктивной нормальной форме. 8. Элиминация конъюнкции. Преобразование: АЙВ =ь А, В. После восьмого этапа формула распадается на множество предложений.
Не все преобразования на этапах 1-8 являются логически эквивалентными. ТЕОРЕМА Если à — множество предложений, полученных из формулы Э, то Я является противоречием тогда и только тогда, когда множество Г невыполнимо. ДОКАЗАТЕЛЬСТВО В доказательстве нуждается шаг 5 — сколемизация. Пусть Р = 1хт... Ч хг т Б хтЯг+тхг+т...
Я„х„А(хт,..., х„) Положим Р':=яхт ...Ухг т Ягьтхг+т...Я„х„А(хт,...,хг т,у(хт, .,хг т),хгет,...,хч) ТЗО Глава 4. Логические исчисления Пусть Р— противоречие;:а К' — не противоречие. Тогда существует интерпретация 1 и набор значений з = (аы...,аг ыаььы..., а„), такой что з*(Р') = И. Положим аг:=Дам...,аг г),зг ..—- (аы...,аг ыаоаг+ы...,а„).Тогда зг(Р) = И и Р— выполнимая формула. П 4.5.4. Правило резолюции для исчисления высказываний Пусть Сг и Сз — два предложения в исчислении высказываний, и пусть Сг = Р ч' С(, а Сз = ~Р Н Сз, где Р— пропозициональная переменная, а С(, Сев любые предложения (в частности, может быть, пустые или состоящие только из одного литерала). Правило вывода С,' НС' называется правилом резолюции.
Предложения Сг н Сз называются резольвируемыми (илн родительскими), предложение С( 'ч' Сз — резольвентой, а формулы Р и — Р— контрарными литералами. Правило резолюции — это очень мощное правило вывода. Многие ранее рассмотренные правила являются частными случаями правила резолюции: А, АчВ В АмВ, ВчС В -А'ч'С А ч'В,. АЧВ В А,А-ьВ Мог(цз ропепз А~В,В+С Транзитивность АЧВ,А~В Слияние ТЕОРЕМА Правило резолюции логично, то есть резольвента является логическим следствием резольвируемыл предлолсеггий доказатнльство Пусть 1(Сг) = И и 1(Сз) = И.
Тогда, если 1(Р) = И, то Сз Ф о и 1(Сз) = И, а значит, 1(С( ч Сз) = И. Если же 1(Р) = Л, то С,' ~ ю и 1(С() = И, а значит, 1(С,' гс,) =И. 0 ЗАМЕЧАНИЕ Резольяента является предложением. ЗАМЕЧАНИЕ Множество формул Г невыполнимо — зто означает, что множество Г пе имеет модели, то есть яе существует интерпретации, в которой ясе формулы Г имели бы значение И.
1З1 4.5. Автоматическое доказательство теорем 4.5.5. Правило резолюции для исчисления предикатов Для применения правила резолюции нужны контрарные литералы в резольвируемых предложениях. Пусть Ст и Сз — два предложения в исчислении предикатов. Правило вывода сг, Сз (С, ч С,),Л называется правилом резолюции в исчислении предикатов, если в предложениях Ст и Сз существуют унифицируемые контрарные литералы Р, и Рго то есть Ст = Рт ц С', и Сз = Рз ц Са, причем атомарные формулы Р, и Рз являются уиифицируемыми наиболее общим унификатором о. В атом случае резольвентой предложений Сг и Сз является предложение (С,' и Са)о, полученное из предложения, С,' тг Сз применением унификатора о. 4.5.6.
Опровержение методом резолюций Опровержение методом резолюций — зто алгоритм автоматического доказательства теорем в прикладном исчислении преднкатов, который сводится к следующему. Пусть нужно установить выводимость Я1- С. Каждая формула множества Я и формула "С (отрицание целевой теоремы) независимо преобразуются в множества предложений. В полученном совокупном множестве предложений С отыскиваются резольвнруемые предложения, к ним применяется правило'резолюпий и резольвента добавляется в множество до тех пор, пока не будет получено пустое предложение. При этом возможны трн случая: 1.
Среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, то есть формула С не выводима из множества формул Я. 2. В результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказана, то есть Я ~- С. 3. Процесс не заканчивается, то есть множество предложений пополняется все новыми резольвентами, среди которых нет пустых. Это ничего не означает. ЗАМЕЧАНИЕ таким образом, исчисление преднкатов является нолуразрешнмой теорией, а метод резолюций является частичным алгоритмом автоматического доказательства теорем.
Пример Докажем методом резолюций теорему Нс (((А ч В) + А) -+ А). Сначала нужно преобразовать в предложения отрицание целевой формулы - (((А — г В) -+ А) -+ А). 1Зг Глава 4. Логические исчисления 1; (-1(. ( АЧВ)ЧА)ЧА). 2. (((Ай- В) ЧА)й-А). 3-6. Формула без изменений. 7. (АгА)4с( ВнА)4с А. 8. АчА, Вь'А,-А. После этого проводится резольвирование имеющихся предложений 1-3.
1. АЧА. 2. -В ч'А. 3.. А. из 1 н 3 по правилу резолюции. из 3 и 4 по правилу резолюции. 4. А 5. П Таким образом, теорема доказана. 4.5.7. Алгоритм метода резолюций Алгоритм поиска опровержения методом резолюций проверяет выводимость формулы С из множества формул Я. Алгоритм 4.2. Метод резолюций Вход: множество предложений С, полученных из множества формул Я и формулы С. Выход: 1 — если С выводимо из Я, Π— е противном случае. М: = С ( М вЂ” текущее множество предложений ) ч Ые П й М до Сйоозе(М, см сз, р,,р2, гг) ( выбор родительских предложений ) !Г см сз = о реп гегмга О ( нечего резольвирозать ) еай 1Е с: = В(см сю р„рт, гг) ( вычисление резольеенты ) М: = М 1.1 (с) ( пополнение текущего множества ) еод и4п!е гесегл 1 ( теорема доказана ) овосноваиив Если алгоритм заканчивает свою работу, то правильность результата очевидным образом следует из теорем предшествующих разделов.
Вообще говоря, эавершаемость этого алгоритма не.гарантирована. П В этом алгоритме использованы две вспомогательные функции. Функция И вычисляет резольвенту двух предложений с1 и сз, содержащих унифицируемые контрарные'литералы рг и рз, соответственно; при этом о — наиболее общий унификатор. Результатом работы функции является резольвента. Процедура С11оозе' выбирает в текущем множестве предложений М два резольвируемых предложения, то есть два предложения, которые содержат унифицируемые контрарные литералы.
Если таковые есть, то процедура их возвращает, 1ЗЗ Упражнения в противном случае возвращается пустое множество. Конкретные реализации процедуры СЬоозе называются стратегиями метода резолюций. ЗАМЕЧАНИЕ В настоящее время прелложеио множество различных стратегий метода резолюций. Среди них рэзличиотся полные и неживые стратегии. Полные стратегии — это такие, которые гарантируют нахождение доказательства теоремы, если оно вообще существует. Неполныс стратегии могут в некоторых случаях не находить доказательства, зато онв работают быстрее.
Следует иметь в виду, что автоматическое доказательство теорем методом резолюций имеет во существу переборный характер, и этот перебор столь велик, что может быть практически неосуществим эа приемлемое время. ОТСТУПЛЕНИЕ При автоматическом доказательстве теорем методом резолюций львиная доля вычислений прихолится на поиск уиифицируемых предложений. Таким образом, эффективная реализация алгоритма унификации критически важна для практической применимости метода резолюций. Комментарии Здесь изложены элементарные сведения из математической логики, причем технически сложные доказательства опущены.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
