Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 87
Текст из файла (страница 87)
Сравнение декларативного и процедурного подходов к искусственному интеллекту было проведено Боденом [145). Незатухаюгцие дебаты между приверженцами этих двух подходов снова оживились, в частности, после публикации [192) и [1145). Сама логика имеет свои истоки в древнегреческой философии и математике.
Фрагменты с изложением различных логических принципов (связывающих синтаксическую структуру высказываний с их истинным или ложным значением, с их смыслом или с допустимостью доводов, в которых они фигурируют) встречаются во многих трудах Платона. Первое известное систематическое исследование логики было проведено Аристотелем, работы которого были собраны его учениками после его смерти в 322 до н.э. в виде трактата, называемого Органон, гк Силлогизмы Аристотеля представляли собой то, что мы теперь называем правилами логического вывода. Хотя силлогизмы включали элементы и пропозициональной логики, и логики 334 Часть П1. Знания и рассуждения первого порядка, сама система Аристотеля в целом была очень слабой с точки зрения современных стаипартов.
В ней не было места для шаблонов логического вывода, которые могли бы применяться к высказываниям с произвольной сложностью, как в современной пропозициональной логике. Тесно связанные со школой Аристотеля мегарская и стоическая школы (которые зародились в пятом веке до н.э. и продолжали свою работу в течение нескольких столетий) ввели в научный обиход принципы систематического исследования импликации и других основных конструкций, до сих пор используемых в современной пропозициональной логике.
Применение истинностных таблиц для определения логических связок было впервые предложено в трудах Филона из Мегары. Стоики приняли к использованию пять основных правил логического вывода как допустимые без доказательства, в том числе правило, которое теперь принято называть правилом отделения (Мог(цз Ропепз). Из этих пяти правил они вывели множество других правил, используя, кроме других принципов, теорему дедукции (с. 302), и имели гораздо более четкое представление о таком понятии, как доказательство, чем Аристотель. Стоики утверждали, что их логика была полной в том смысле, что они смогли описать все допустимые правила логического вывода, но от их трудов остались лишь отдельные фрагменты, по которым трудно судить об их правоте.
Хорошее описание истории развития логики на примере мегарской и стоической школ, в той степени, в какой эти школы нам известны, приведено в работе Бенсона Мэйтса [1000]. Идеи о том, что логический вывол можно свести к чисто механическому процессу, применяемому к формальному языку, были высказаны Готфридом Вильгельмом Лейбницем (1646 — 1716). Однако собственные работы Лейбница в области математической логики обладали серьезными недостатками, поэтому он запомнился скорее как человек, выдвинувший эти идеи как цели, которые должны быть достигнуты, а ие действительно предпринявший результативную попытку их достичь. Джордж Буль [149] впервые представил полную и работоспособную систему формальной логики в своей книге Тйе Майешийса( Апа1ут оГ7од(с.
Логика Буля была почти полностью промоделирована на основе обычной алгебры действительных чисел, и в ней в качестве основного метода логического вывода использовалась подстановка логически эквивалентных выражений. Хотя систему Буля еше нельзя было считать полной пропозициональной логикой, она оказалась настолько близкой к таковой, что другие математики сумели быстро заполнить все недостаюшие части. Шредер [1368] описал конъюнктивную нормальную форму, тогда как хорновская форма была введена намного позднее Альфредом Хорном [675]. Первое полное описание современной пропозициональной логики (и логики первого порядка) можно найти в книге Ве» (77зсйг[г7 (" Система обозначения понятий") Готтлоба Фреге [496]. Первое механическое устройство для формирования логических выводов было сконструировано потомственным графом Стенхоупом (1753 — 1816).
Машина Стенхоупа, Оешопзггагог, была способна обрабатывать силлогизмы и некоторые логические выводы в теории вероятностей. Уильям Стэнли Джевонс, один из тех, кто усовершенствовал и расширил результаты Буля, сконструировал в 1869 году "логическое фортепьяно" для формирования выводов в булевой логике. Занимательная и поучительная история этих и других ранних механических устройств для формирования рассуждений описана Мартином Гарднером [519]. Первой опубликованной компьютерной программой для формирования логического вывода была разработанная Ньюэллом, Шоу и Саймоном программа [.о81с Т)зеог)зз [1127].
Эта Глава 7. Логические агенты 335 программа была предназначена для моделирования мыслительных процессов человека. Программа, позволяющая сформировать доказательство, была фактически спроектирована в 1954 году Мартином Дэвисом [334], но результаты работ в области создания программы ].о8!с Т[зеог[зг бьши опубликованы немного раньше. И программа Дэвиса от 1954 года, и программа ].о81с Т[зеог[зг были основаны на достаточно произвольно выбранных методах, которые не оказали существенного влияния на дальнейшие работы в области автоматизированного дедуктивного вывода.
Истинностные таблицы как метод проверки допустимости или невыполнимости высказываний в языке пропозициональной логики были введены в арсенал ученых независимоЛюдвигом Витггенштейном [1607] и Эмилем Постом [1231]. В 1930-х годах большие успехи были достигнугы в области создания методов логического вывода для логики первого порядка.
В частности, Гедель [565] показал, что полная процедура логического вывода в логике первого порядка может быть получена путем сведения к пропозициональной логике с использованием теоремы Эрбрана [650]. Мы снова вернемся к этой теме в главе 9, а здесь необходимо сделать важное замечание о том, что разработка эффективных пропозициональных алгоритмов в 1960-х годах мотивировалась в основном стремлением математиков создать эффективные средства доказательства теорем для логики первого порядка. Алгоритм Дэвиса— Патнем [336] был первым эффективным гшгорнтмом логического вывода в пропозициональной логике, но в большинстве случаев обладал меньшей эффективностью по сравнению с алгоритмом поиска с возвратами Ррьь, который был введен двумя годами позже [335]. Полное правило резолюции и доказательство его полноты было опубликовано в оригинальной статье Дж.Э. Робинсона [1298], который также показал, как может осушествляться формирование рассуждений в логике первого порядка без обращения к пропозициональным методам.
Стефен Кук [289] показал, что задача определения выполнимости высказывания в пропозициональной логике является ХР-полной. Поскольку определение того, является ли высказывание логическим следствием, эквивалентно задаче определения его невыполнимости, эта задача является ко-]ЧР-полной. Известны многие подмножества пропозициональной логики, для которых задача проверки выполнимости решается за полиномиальное время; одним из таких подмножеств являются хорновские выражения. Алгоритм прямого логического вывода для хорновскнх выражений с линейными затратами времени предложен Доулингом и Галльером [407], которые описали свой алгоритм в виде процесса обработки потока данных, подобного распространению сигналов в логической схеме. Задача проверки выполнимости стала одним из канонических примеров сведения к ХР-полным задачам; например, Кайе [782] показал, что игра М[пезвеерег (минный тральщик) (см.
упр. 7.11) является ХР-полной. Попытки применения алгоритмов локального поиска для решения задач проверки выполнимости предпринимались различными авторами на протяжении всех 1980-х годов; все эти алгоритмы были основаны на идее минимизации количества невыполненных выражений [614]. Особенно эффективный алгоритм был разработан Гу [601] и независимо от него Селманом и др. [1382], которые назвали этот алгоритм СВАТ и показали, что он способен решать широкий перечень очень трудных задач сочень большой скоростью.
Алгоритм Ыа2)сЯАт, описанный в этой главе, также предложен Селманом и др. [1380]. 336 Часть П1. Знания и рассуждения "Фазовый переход" в процессе определения выполнимости сформированных случайным образом задач [с-ЬАТ впервые был обнаружен Саймоном и Дюбуа [1421]. Эмпирические результаты, полученные Кроуфордом и Отоном [307], свидетельствуют о том, что при решении крупных сформированных случайным образом задач 3-БАТ это резкое изменение характеристик возникает в диапазоне значений отношения "высказывание/переменная", приближающихся к 4,24; кроме того, в этой статье описана очень эффективная реализация алгоритма 0рт,г..
Байардо и шрэг [87] описали еше одну эффективную реализацию алгоритма пят т с использованием методов из области удовлетворения ограничений, а в [1090] описан алгоритм С1за]Г, который решает задачи проверки аппаратного обеспечения с миллионом переменных, ставший победителем конкурса БАТ 2002.
Ли и Энбулаган [926] описали эвристики, основанные на распространении единичных выражений, позволяющие создавать быстрые решатели задач. Чизман и др. [244] предоставили данные о многих задачах, связанных с задачами проверки выполнимости, и пришли к выводу, что все ХР-трудные задачи обнаруживают фазовый переход. Керкпатрик и Селман [800] показали, каким образом можно использовать методы статистической физики для получения представления о том, какова точная "форма" фазового перехода.
Теоретический анализ его местонахождения все еше довольно неудовлетворнтелен: до сих пор удалось локазать лишь то, что для случайно сформированных задач 3-ЬАТ фазовьш переход находится в диапазоне 13 . 003, 4. 5981. Кук и Митчелл [290] составили превосходный обзор результатов по этой и некоторым другим темам, касающимся выполнимости.
Самые ранние теоретические исследования показали, что алгоритм 1эРт.ь применительно к некоторым естественным распределениям задач характеризуется в среднем полиномиальной сложностью. Этот факт, который мог бы, в принципе, стать предметом восхищения, начал казаться менее восхитительным, когда Франко и Паулл [494] показали, что те же задачи можно было бы решить за постоянное время, просто проверяя случайно выбранные варианты присваивания. Метод случайной выработки вариантов, описанный в данной главе, приводит к получению гораздо более трудных задач. Заинтересовавшись достигнутым на практике успехом в использовании локального поиска при решении таких задач, Кутсупиас и Пападимитриу [848] показали, что простой алгоритм восхождения к вершине способен решать почти все экземпляры задачи проверки выполнимости очень быстро, а это свидетельствует о том, что трудные задачи встречаются редко. Более того, Шенинг [1365] продемонстрировал рандомизированный вариант алгоритма ОБАТ, для которого ожидаемое время прогона в худшем случае при решении задач 3-$АТ составляет з .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
