БИБЛИОГРАФИЧЕСКИЕ И ИСТОРИЧЕСКИЕ ЗАМЕТКИ
Понятие агента, который использует процесс формирования логических рассуждений для установления связи между восприятиями и действиями, было выдвинуто в статье Джона Маккарти "Programs with Common Sense" [1009], [1011]. Кроме того, Маккарти стал основоположником декларативного подхода, указав, что очень изящным является такой способ создания программного обеспечения, который предусматривает передачу агенту указаний о том, что он должен знать. В статье Аллена Ньюэлла "The Knowledge Lever [1124] подчеркнуто, что рациональные агенты могут быть описаны и проанализированы на абстрактном уровне, определяемом знаниями, которым они обладают, а не программами, которые в них выполняются. Сравнение декларативного и процедурного подходов к искусственному интеллекту было проведено Боденом [145]. Незатухающие дебаты между приверженцами этих двух подходов снова оживились, в частности, после публикации [192] и [1145].
Сама логика имеет свои истоки в древнегреческой философии и математике. Фрагменты с изложением различных логических принципов (связывающих синтаксическую структуру высказываний с их истинным или ложным значением, с их смыслом или с допустимостью доводов, в которых они фигурируют) встречаются во многих трудах Платона. Первое известное систематическое исследование логики было проведено Аристотелем, работы которого были собраны его учениками после его смерти в 322 до н.э. в виде трактата, называемого Органон. Силлогизмы Аристотеля представляли собой то, что мы теперь называем правилами логического вывода. Хотя силлогизмы включали элементы и пропозициональной логики, и логики первого порядка, сама система Аристотеля в целом была очень слабой с точки зрения современных стандартов. В ней не было места для шаблонов логического вывода, которые могли бы применяться к высказываниям с произвольной сложностью, как в современной пропозициональной логике.
Тесно связанные со школой Аристотеля мегарская и стоическая школы (которые зародились в пятом веке до н.э. и продолжали свою работу в течение нескольких столетий) ввели в научный обиход принципы систематического исследования импликации и других основных конструкций, до сих пор используемых в современной пропозициональной логике. Применение истинностных таблиц для определения логических связок было впервые предложено в трудах Филона из Мегары. Стоики приняли к использованию пять основных правил логического вывода как допустимые без доказательства, в том числе правило, которое теперь принято называть правилом отделения (Modus Ponens). Из этих пяти правил они вывели множество других правил, используя, кроме других принципов, теорему дедукции (с. 302), и имели гораздо более четкое представление о таком понятии, как доказательство, чем Аристотель. Стоики утверждали, что их логика была полной в том смысле, что они смогли описать все допустимые правила логического вывода, но от их трудов остались лишь отдельные фрагменты, по которым трудно судить об их правоте. Хорошее описание истории развития логики на примере мегарской и стоической школ, в той степени, в какой эти школы нам известны, приведено в работе Бенсона Мэйтса [1000].
Идеи о том, что логический вывод можно свести к чисто механическому процессу, применяемому к формальному языку, были высказаны Готфридом Вильгельмом Лейбницем (1646—1716). Однако собственные работы Лейбница в области математической логики обладали серьезными недостатками, поэтому он запомнился скорее как человек, выдвинувший эти идеи как цели, которые должны быть достигнуты, а не действительно предпринявший результативную попытку их достичь.
Джордж Буль [149] впервые представил полную и работоспособную систему формальной логики в своей книге The Mathematical Analysis of Logic. Логика Буля была почти полностью промоделирована на основе обычной алгебры действительных чисел, и в ней в качестве основного метода логического вывода использовалась подстановка логически эквивалентных выражений. Хотя систему Буля еще нельзя было считать полной пропозициональной логикой, она оказалась настолько близкой к таковой, что другие математики сумели быстро заполнить все недостающие части. Шрёдер [1368] описал конъюнктивную нормальную форму, тогда как хорновская форма была введена намного позднее Альфредом Хорном [675]. Первое полное описание современной пропозициональной логики (и логики первого порядка) можно найти в книге Begriffschrift ("Система обозначения понятий") Готтлоба Фреге [496].
Первое механическое устройство для формирования логических выводов было сконструировано потомственным графом Стенхоупом (1753-1816). Машина Стен-хоупа, Demonstrator, была способна обрабатывать силлогизмы и некоторые логические выводы в теории вероятностей. Уильям Стэнли Джевонс, один из тех, кто усовершенствовал и расширил результаты Буля, сконструировал в 1869 году "логическое фортепьяно" для формирования выводов в булевой логике. Занимательная и поучительная история этих и других ранних механических устройств для формирования рассуждений описана Мартином Гарднером [519]. Первой опубликованной компьютерной программой для формирования логического вывода была разработанная Ньюэллом, Шоу и Саймоном программа Logic Theorist [1127]. Эта программа была предназначена для моделирования мыслительных процессов человека. Программа, позволяющая сформировать доказательство, была фактически спроектирована в 1954 году Мартином Дэвисом [334], но результаты работ в области создания программы Logic Theorist были опубликованы немного раньше. И программа Дэвиса от 1954 года, и программа Logic Theorist были основаны на достаточно произвольно выбранных методах, которые не оказали существенного влияния на дальнейшие работы в области автоматизированного дедуктивного вывода.
Истинностные таблицы как метод проверки допустимости или невыполнимости высказываний в языке пропозициональной логики были введены в арсенал ученых независимо Людвигом Виттгенштейном [1607] и Эмилем Постом [1231]. В 1930-х годах большие успехи были достигнуты в области создания методов логического вывода для логики первого порядка. В частности, Гёдель [565] показал, что полная процедура логического вывода в логике первого порядка может быть получена путем сведения к пропозициональной логике с использованием теоремы Эрбрана [650]. Мы снова вернемся к этой теме в главе 9, а здесь необходимо сделать важное замечание о том, что разработка эффективных пропозициональных алгоритмов в 1960-х годах мотивировалась в основном стремлением математиков создать эффективные средства доказательства теорем для логики первого порядка. Алгоритм Дэвиса— Патнем [336] был первым эффективным алгоритмом логического вывода в пропозициональной логике, но в большинстве случаев обладал меньшей эффективностью по сравнению с алгоритмом поиска с возвратами DPLL, который был введен двумя годами позже [335]. Полное правило резолюции и доказательство его полноты было опубликовано в оригинальной статье Дж.Э. Робинсона [1298], который также показал, как может осуществляться формирование рассуждений в логике первого порядка без обращения к пропозициональным методам.
Стефен Кук [289] показал, что задача определения выполнимости высказывания в пропозициональной логике является NP-полной. Поскольку определение того, является ли высказывание логическим следствием, эквивалентно задаче определения его невыполнимости, эта задача является KO-NP-ПОЛНОЙ. Известны многие подмножества пропозициональной логики, для которых задача проверки выполнимости решается за полиномиальное время; одним из таких подмножеств являются хорновские выражения. Алгоритм прямого логического вывода для хорновских выражений с линейными затратами времени предложен Доулингом и Галльером [407], которые описали свой алгоритм в виде процесса обработки потока данных, подобного распространению сигналов в логической схеме. Задача проверки выполнимости стала одним из канонических примеров сведения к NP-полным задачам; например, Кайе [782] показал, что игра Minesweeper (минный тральщик) (см. упр. 7.11) является NP-полной.
Попытки применения алгоритмов локального поиска для решения задач проверки выполнимости предпринимались различными авторами на протяжении всех 1980-х годов; все эти алгоритмы были основаны на идее минимизации количества невыполненных выражений [614]. Особенно эффективный алгоритм был разработан Гу [601] и независимо от него Селманом и др. [1382], которые назвали этот алгоритм GSAT и показали, что он способен решать широкий перечень очень трудных задач сочень большой скоростью. Алгоритм WalkSAT, описанный в этой главе, также предложен Селманом и др. [1380].
"Фазовый переход" в процессе определения выполнимости сформированных случайным образом задач k-SAT впервые был обнаружен Саймоном и Дюбуа [1421]. Эмпирические результаты, полученные Кроуфордом и Отоном [307], свидетельствуют о том, что при решении крупных сформированных случайным образом задач 3-SAT это резкое изменение характеристик возникает в диапазоне значений отношения "высказывание/переменная", приближающихся к 4,24; кроме того, в этой статье описана очень эффективная реализация алгоритма DPLL. Байардо и Шрэг [87] описали еще одну эффективную реализацию алгоритма DPLL с использованием методов из области удовлетворения ограничений, а в [1090] описан алгоритм Chaff, который решает задачи проверки аппаратного обеспечения с миллионом переменных, ставший победителем конкурса SAT 2002. Ли и Энбулаган [926] описали эвристики, основанные на распространении единичных выражений, позволяющие создавать быстрые решатели задач. Чизман и др. [244] предоставили данные о многих задачах, связанных с задачами проверки выполнимости, и пришли к выводу, что все NP-трудные задачи обнаруживают фазовый переход. Кёр-кпатрик и Селман [800] показали, каким образом можно использовать методы статистической физики для получения представления о том, какова точная "форма" фазового перехода. Теоретический анализ его местонахождения все еще довольно неудовлетворителен: до сих пор удалось доказать лишь то, что для случайно сформированных задач 3-SAT фазовый переход находится в диапазоне [3.003,4.598]. Кук и Митчелл [290] составили превосходный обзор результатов по этой и некоторым другим темам, касающимся выполнимости.
Самые ранние теоретические исследования показали, что алгоритм DPLL применительно к некоторым естественным распределениям задач характеризуется в среднем полиномиальной сложностью. Этот факт, который мог бы, в принципе, стать предметом восхищения, начал казаться менее восхитительным, когда Франко и Па-улл [494] показали, что те же задачи можно было бы решить за постоянное время, просто проверяя случайно выбранные варианты присваивания. Метод случайной выработки вариантов, описанный в данной главе, приводит к получению гораздо более трудных задач. Заинтересовавшись достигнутым на практике успехом в использовании локального поиска при решении таких задач, Кутсупиас и Пападимит-риу [848] показали, что простой алгоритм восхождения к вершине способен решать почти все экземпляры задачи проверки выполнимости очень быстро, а это свидетельствует о том, что трудные задачи встречаются редко. Более того, Шёнинг [1365] продемонстрировал рандомизированный вариант алгоритма GSAT, для которого ожидаемое время прогона в худшем случае при решении задач 3-SAT составляет 1. 333п; этот предел все еще является экспоненциальным, но гораздо более низким по сравнению с достигнутыми ранее пределами для худшего случая. Алгоритмы проверки выполнимости все еще остаются очень активной областью исследования; хорошей отправной точкой для изучения этой темы может служить сборник статей под редакцией Дю и др. [418].
Истоки идей по созданию агентов на основе логических схем можно проследить до оригинальной статьи Мак-Каллока и Питтса [1017], которая послужила началом исследований в области нейронных сетей. Вопреки сложившемуся общему мнению, эта статья касалась реализации проекта агента на основе логической схемы в мозгу. Однако агенты на основе логической схемы долго не привлекали значительного внимания исследователей в области искусственного интеллекта. Самым заметным исключением из этого правила явились работы Стена Розеншайна [760], [1308], который разработал способы компиляции агентов на основе логических схем из декларативных описаний проблемной среды. Логические схемы для обновления высказываний, хранящихся в регистрах, тесно связаны с аксиомой состояния-преемника, разработанной для логики первого порядка Рейтером [1277]. В работах Рода Брукса [189], [190] продемонстрирована эффективность использования проектов на основе логической схемы для управления роботами; к этой теме мы вернемся в главе 25. Брукс [192] утверждает, что для искусственного интеллекта необходимы лишь проекты на основе логических схем, а методы представления и формирования логических рассуждений являются громоздкими, дорогостоящими и ненужными. Но, по мнению авторов, ни один из этих подходов, отдельно взятых, не является достаточным.
Мир вампуса был придуман Грегори Йобом [1633]. Любопытно то, что Йоб разработал этот мир, поскольку ему надоели игры, которые проводятся в мире, представленном в виде квадратной решетки: топология его первоначального мира вампуса представляла собой додекаэдр, а мы снова поместили вампуса в старую скучную квадратную решетку. Майкл Генезерет был первым, кто указал, что мир вампуса можно использовать как испытательную площадку для агентов.