Новиков Ф.А. Дискретная математика для программистов (860615), страница 34
Текст из файла (страница 34)
Пусть нужно установить выводимостьSG.Каждая формула множества S и формула ->G (отрицание целевой теоремы)независимо преобразуются в множества предложений. В полученном совокупном множестве предложений С обыскиваются резольвируемые предложения, кним применяется правило резолюции и резольвента добавляется в множествопредложений до тех пор, пока не будет получено пустое предложение. При этомвозможны три случая:176Глава 4. Логические исчисления1. Среди текущего множества предложений нет резольвируемых или же все резольвенты уже присутствуют в текущем множестве предложений. Это означает, что теорема опровергнута, то есть формула G не выводима из множестваформул S.2.
В результате очередного применения правила резолюции получено пустоепредложение. Это означает, что теорема доказана, то есть S Ь G.3. Процесс не заканчивается, то есть множество предложений пополняется всёновыми резольвентами, среди которых пет пустых. Это ничего не означает.ЗАМЕЧАНИЕТаким образом, исчисление предикатов является полуразрешимой теорией, а метод резолюций является частичным алгоритмом автоматического доказательства теорем.Пример Докажем методом резолюций теорему 1-£ (((Л —> В) —> Л) —• Л).Сначала нужно преобразовать в предложения отрицание целевой формулы-п(((Д -> В)1.2.3-6.7.8.А) -> А).—.(—.(—.(—->1 V В) V А) V А).(((А & ->В) V А) & ->А).Формула без изменений.(Л V Л) & ( - .
£ V Л) & - А .Л V Л , - В V Л,-Л.После этого проводится резольвировапие имеющихся предложений 1-3.1. л v л.2. ->В VЛ.3. - А .4. Лиз 1 и 3 по правилу резолюции.5. •из 3 и 4 по правилу резолюции.Таким образом, теорема доказана.4.5.7. Алгоритм метода резолюцийАлгоритм поиска опровержения методом резолюций проверяет выводимость формулы G из множества формул S.Алгоритм 4.2 Метод резолюцийВход: множество предложений С, полученных из множества формул S и формулы ->G.Выход: True — если G выводимо из S, false — в противном случае.М: = С { М — текущее множество предложений }Комментарии177while [ • ] $ М doChoose(M,ci,c 2 ,pi,p2,с) { выбор родительских предложений }if c\, C2 = 0 thenreturn false { нечего резольвировать — теорема опровергнутаend ifс: = -R(ci,c2,pi,p2,0") { вычисление резольвенты }М : = М + с { пополнение текущего множества }end whilereturn true { теорема доказана }ОБОСНОВАНИЕЕСЛИ алгоритм заканчивает свою работу, то правильность результата очевидным образом следует из теорем предшествующих разделов.
Вообщеговоря, завершаемость этого алгоритма не гарантирована.•В этом алгоритме использованы две вспомогательные функции. Функция R вычисляет резольвенту двух предложений с\ и с 2 , содержащих унифицируемыеконтрарные литералы р\ и р2 соответственно; при этом а — наиболее общийунификатор (см. 4.3.3). Результатом работы функции является резольвента.Процедура Choose выбирает в текущем множестве предложений М два резольвируемых предложения, то есть два предложения, которые содержат унифицируемые контрарные литералы.
Если таковые есть, то процедура их возвращает,в противном случае возвращается пустое множество. Конкретные реализациипроцедуры Choose называются стратегиями метода резолюций.ЗАМЕЧАНИЕВ настоящее время предложено множество различных стратегий метода резолюций. Срединих различаются полные и неполные стратегии. Полные стратегии — это такие, которыегарантируют нахождение доказательства теоремы, если оно вообще существует. Неполные стратегии могут в некоторых случаях не находить доказательства, зато они работаютбыстрее.
Следует иметь в виду, что автоматическое доказательство теорем методом резолюций имеет по существу переборный характер, и этот перебор столь велик, что можетбыть практически неосуществим за приемлемое время.ОТСТУПЛЕНИЕПри автоматическом доказательстве теорем методом резолюций львиная доля вычислений приходится на поиск унифицируемых предложений. Таким образом, эффективнаяреализация алгоритма унификации критически важна для практической применимостиметода резолюций.КомментарииВ этой главе изложены элементарные сведения из математической логики, причёмтехнически сложные доказательства опущены.
Более подробное изложение можно найти в многочисленных классических учебниках, таких как [30]. Классическое описание автоматического доказательства теорем методом резолюций име-178Глава 4. Логические исчисленияется в [29]. Эта книга содержит описание различных стратегий и усовершенствований метода резолюций, а также многочисленные примеры применений. Алгоритмы 4.1 и 4.2 являются упрощенными модификациями алгоритмов, описанныхв [29].УпражненияDef4.1. Пусть х = у = (х —• у) к (у —»• х). Доказать, что формуласодержащаятолько связку =, является тавтологией тогда и только тогда, когда каждаяпеременная входит в неё чётное число раз.4.2.
Описать процедуру, которая перечисляет множество термов для заданныхконечных множеств переменных, констант и функциональных символов.4.3. Пусть некоторая формула А теории £ — не тавтология. Обозначим черезА множество всех частных случаев формулы А.
Определим теориюдобавив к исчислению высказываний все частные случаи формулы А в качестве аксиом:= L U А. Доказать, что теорияпротиворечива, то естьсуществует такая формула В, чтоВ и Ь £ + -*В.4.4. Доказать, что формула (Vx (А) (х) —• Vx (В(х))) —• (Vx (А(х) —> £(х)))общезначима.4.5. Доказать методом резолюций: h^ А —> (В —> А к В).Глава 5КомбинаторикаПредмету комбииаторики не так просто дать краткое исчерпывающее определение. В некотором смысле слово «комбинаторика» можно понимать как синонимтермина «дискретная математика», то есть исследование дискретных конечныхматематических структур.
На школьном уровне с термином «комбинаторика»связывают просто набор известных формул, служащих для вычисления так называемых комбинаторных чисел, о которых идёт речь в первых разделах этойглавы. Может показаться, что эти формулы полезны только для решения олимпиадпых задач и не имеют отношения к практическому программированию. Насамом деле это далеко пе так. Вычисления на дискретных конечных математических структурах, которые часто называют комбинаторными вычислениями,требуют комбинаторного анализа для установления свойств и выявления оценкиприменимости используемых алгоритмов.
Рассмотрим элементарный жизненныйпример.Пример Пусть некоторое агентство недвижимости располагает базой данныхиз п записей, причём каждая запись содержит одно предложение (что имеется)и один запрос (что требуется) относительно объектов недвижимости. Требуетсянайти все такие пары записей, в которых предложение первой записи совпадает с запросом второй и одновременно предложение второй записи совпадает сзапросом первой. (На бытовом языке это называется подбором вариантов обмена.) Допустим, что используемая СУБД позволяет проверить вариант за однумиллисекунду.
Нетрудно сообразить, что при «лобовом» алгоритме поиска вариантов (каждая запись сравнивается с каждой) потребуется п(п— 1)/2 сравнений.Если п = 100, то все в порядке — ответ будет получен за 4,95 секунды. Но еслип = 100 ООО (более реальный случай), то ответ будет получен за 4 999 950 секунд,что составляет без малого 1389 часов и вряд ли может считаться приемлемым.Обратите внимание на то, что мы оценили только трудоёмкость подбора прямыхвариантов, а существуют ещё варианты, когда число участников сделки большедвух...180Глава 5. Комбинаторика'Этот пример показывает, что практические задачи и алгоритмы требуют предварительного анализа и количественной оценки.
Задачи обычно оцениваютсяс точки зрения размера, то есть общего количества различных вариантов, среди которых нужно пайти решение, а алгоритмы оцениваются с точки зрениясложности. При этом различают сложность по времени (или временную сложность), то есть количество необходимых шагов алгоритма, и сложность по памяти (или емкостную сложность), то есть объём памяти, необходимый для работыалгоритма.Во всех случаях основным инструментом такого анализа оказываются формулыи методы, рассматриваемые в этой главе.5.1.
Комбинаторные задачиВо многих практических случаях возникает необходимость подсчитать количество возможных комбинаций объектов, удовлетворяющих определённым условиям. Такие задачи называются комбинаторными. Разнообразие комбинаторныхзадач не поддаётся исчерпывающему описанию, но среди них есть целый рядособенно часто встречающихся, для которых известны способы подсчёта.5.1.1. Комбинаторные конфигурацииДля формулировки и решения комбинаторных задач используются различныемодели комбинаторных конфигураций. Рассмотрим следующие две наиболее популярные:1. Дано п предметов.
Их нужно разместить по га ящикам так, чтобы выполнялисьзаданные ограничения. Сколькими способами это можно сделать?2. Рассмотрим множество функцийF: X —>Y,где |Х| = п, |У| = га.Не ограничивая общности, можно считать, чтоХ = {1 , . . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
