Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 115
Текст из файла (страница 115)
В подходе на основе натуральной дедукции (па!ига! с(ег]цсг!оп), который был введен Герхардом Генценом [541] и Станиславом Яськовским [725], основное внимание было сосредоточено не на аксиоматических системах, а на правилах логического вывода. Натуральная дедукция получила название натуральной", поскольку в ней не требуется преобразование в нормальную форму (неудобную для восприятия человеком), а также в связи с тем, что в ней применяются такие правила логического вывода, которые кажутся естественными для людей. Правитц [! 235] посвятил описанию натуральной дедукции целую книгу. Галье [515] применил подход Гентцена для разъяснения теоретических основ автоматизированной дедукции.
Крайне важным этапом в разработке глубокого математического анализа логики первого порядка явилось изобретение формы представления в виде импликационных выражений (с!ацза1 !огт). Уайтхед и Рассел [1584] описали так называемые правила прохождения (ги1ез о( раззайе) (фактически этот термин принадлежит Эрбрану [650]), которые используются для перемешения кванторов в переднюю часть формул. Торальфом Сколемом [1424] были достаточно своевременно предложены сколемовские константы и сколемовские функции.
Общая процедура сколемизации, наряду с важным понятием универсума Эрбрана, описана в [1425]. Крайне важную роль в разработке автоматизированных методов формирования рассуждений, как до, так и после введения Робинсоном правила резолюции, играет теорема Эрбрана, названная в честь французского логика Жака Эрбрана [650]. Это отражается в применяемом нами термине "универсум Эрбрана", а не "универсум Сколема", даже несмотря на то, что это понятие в действительности было открыто Сколемом.
Кроме того, Эрбран может считаться изобретателем операции унификации. Гедель [565], опираясь на идеи Сколема и Эрбрана, сумел показать, что для логики первого порядка имеется полная процедура доказательства. Алан Тьюринг [!518] и Алонсо Черч [255[ практически одновременно продемонстрировали, используя очень разные доказательства, что задача определения общезначимости в логике первого порядка не имеет решения.
В превосходной книге Эндертона [438] все эти результаты описаны в строгой, но труднодоступной для понимания манере. Хотя Маккарти [!009] предложил использовать логику первого порядка для представления знаний и формирования рассуждений в искусственном интеллекте, первые подобные системы были разработаны логиками, заинтересованными в получе- Глава 9.
Логический вывод в логике первого порядка 431 нии средств автоматического доказательства математических теорем. Впервые применение метода пропозиционализации и теоремы Эрбрана предложено Абрахамом Робинсоном, а Гилмор [556] написал первую программу, основанную на этом подходе. Дэвис и Патнем [336] применили форму представления в виде импликационных выражений и разработали программу, в которой предпринимались попытки поиска противоречий путем подстановки элементов универсума Эрбрана вместо переменных для получения базовых выражений, а затем поиска пропозициональных противоречивостей среди этих базовых выражений. Правиц [1234] разработал ключевую идею, позволяющую использовать для управления процессом поиска тенденцию к обнаружению пропозициональных противоречивостей и вырабатывать термы из универсума Эрбрана, только если это необходимо для определения пропозициональной противоречивости.
После дальнейшей разработки этой идеи другими исследователями Дж.Э. Робинсон (который не связан родством с Абрахамом Робинсоном) пришел к созданию метода резолюции [1298]. Примерно в то же время советским исследователем С. Масловым [994], [995] на основе немного иных принципов был разработан так называемый инверсныйметод, который характеризуется некоторыми вычислительными преимуществами над пропозиционализацией. Метод соединения Вольфганга Бибеля [123] может рассматриваться как расширение этого подхода. После разработки метода резолюции исследования в области логического вывода первого порядка стали развиваться в нескольких разных направлениях.
В искусственном интеллекте метод резолюции применялся для создания систем поиска ответов на вопросы Корделлом Грином и Бертрамом Рафаэлем [593]. Несколько менее формальный подход был принят Карлом Хьюиттом [651]. Разработанный им язык Р!аппег, хотя и не был полностью реализован, явился предшественником логического программирования и включал директивы для прямого и обратного логического вывода и для отрицания как недостижения цели. А подмножество этого языка, известное как М!его-Р]аппег [1475], было реализовано и использовалось в системе понимания естественного языка 8]зп]1ц [160 !].
В ранних реализациях систем искусственного интеллекта большие усилия направлялись на разработку структур данных, которые должны были обеспечить эффективную выборку фактов; эти работы описаны в книгах по программированию для искусственного интеллекта [240], ]479], ]1148]. В начале 1970-х годов в искусственном интеллекте полностью утвердился метод прямого логического вывода как легко доступная пониманию альтернатива методу резолюции. Прямой логический вывод использовался в самых различных системах, начиная от программы автоматического доказательства геометрических теорем Невинса [1123] и заканчивая экспертной системой В! для разработки конфигурации компьютеров ЧАХ ]1026]. Приложения искусственного интеллекта обычно охватывают большое количество правил, поэтому было важно разработать эффективную технологию согласования с правилами, особенно для инкрементных обновлений.
Для поддержки таких приложений была разработана технология продукционных систем. Язык продукционных систем Ора-5 [197], ]482] использовался для экспертной системы В1 и для когнитивной архитектуры Боаг [880]. В язык Орз-5 был включен процесс согласования с помощью ге!е-алгоритма [483]. Архитектура Боаг, позволяющая вырабатывать новые правила для кэширования результатов предыдущих вычислений, способна создавать очень большие множества правил; например, в системе ТасА!г-боаг, предназначенной для управления тренажером, моделирующим самолет-истребитель [743], количество правил превышало один миллион.
Язык 432 Часть !1!. Знания и рассуждения С[.!РБ [!626] продукционных систем на основе языка С, разработанный в !ЧАБА, обеспечивал лучшую интеграцию с другими программными, аппаратными и сенсорными системами и использовался для автоматизации космической станции и разработки нескольких военных приложений. Большой вклад в понимание особенностей прямого логического вывода внесли также работы в области исследований, известной как дедуктивные базы данных.
Исследования в этой области начались с симпозиума, организованного в Тулузе в 1977 году Джеком Минкером, который собрал вместе специалистов в области логического вывода и систем баз данных [514]. В опубликованном сравнительно недавно историческом обзоре [1264] сказано: "Дедуктивные системы [баз данных) были попыткой адаптировать язык Рго!о8, воплощающий видение мира с «малыми данными», к миру «больших данных»". Таким образом, цель разработок в этой области состоит в объединении технологии баз данных, которая предназначена для выборки больших множеств фактов, с технологией логического вывода на основе языка Рго!о8, в которой обычно осуществляется выборка одновременно только одного факта. К числу работ в области дедуктивных баз данных относятся ]228] и [1525].
Важная работа, выполненная Чандрой и Нарелом ]23 !], а также Ульманом [1524], привела к признанию языка Оага!о8 в качестве стандартного языка для дедуктивных баз данных. Кроме того, стал стандартным "восходящий" логический вывод, или прямой логический вывод, отчасти потому, что данный метод позволяет избежать проблем, обусловленных незавершаемыми и избыточными вычислениями, которые возникают при обратном логическом выводе, и отчасти потому, что имеет более естественную реализацию в терминах основных операций реляционной базы данных. Разработка метода магических множеств для перезаписи правил Бансильоном и др. ]67] позволила воспользоваться в прямом логическом выводе преимушествами целенаправленности, свойственными обратному логическому выводу. Методы табулированного логического программирования (с, 1), вступившие в конкурентную борьбу с другими методами, заимствовали преимушества динамического программирования от прямого логического вывода.
Большой вклад в понимание сложностей логического вывода внесло сообщество пользователей дедуктивных баз данных. Чандра и Мерлин ]232] впервые показали, что задача согласования единственного нерекурсивного правила (в терминологии баз данных — съ конъюнктивного запроса) может оказаться )чР-трудной. Купер и Варди [870] предложили использовать понятие сь сложности данных (т.е. сложности как функции размера базы данных, в которой размер правила рассматривается как постоянный) в качестве подходящего критерия эффективности получения ответов на запросы.
Готтлоб и др. [586] обсудили связь между конъюнктивными запросами и задачами удовлетворения ограничений, показав, как можно использовать способ декомпозиции гипердерева для оптимизации процесса согласования. Как уже упоминалось выше, процедуры обратного логического вывода, применяемые для логического вывода, впервые появились в разработанном Хьюиттом языке Р1аппег ]651].
Но логическое программирование как таковое развивалось независимо от этого направления разработок. Ограниченная форма линейной резолюции, называемая еь ВЬ-резолюцией, была разработана Ковальским и Кюнером [853] на основе метода устранения моделей Лавленда [947]; после применения этого метода к определенным выражениям он принял вид метода 'а. БЬР-резолюции, который предоставил возможность осуществлять интерпретацию определенных выражений как про- Глава 9. Логический вывод в логике первого порядка 433 грамм [849 — 851).
Между тем в 1972 году французский исследователь Ален Колмерор разработал и реализовал Рго]ой в целях синтаксического анализа текста на естественном языке; первоначально выражения Рго1о8 предназначались для использования в качестве правил контекстно-свободной грамматики [285), [!311). Основная часть теоретических основ логического программирования разработана Ковальским в сотрудничестве с Колмерором.
Семантическое определение с использованием наименьших фиксированных точек предложено Ван Эмденом и Ковальским [1530]. Ковальский и Коэн [274], [852] подготовили хорошие исторические обзоры истоков языка Рго!о8. Теоретический анализ основ языка Рго!о8 и других языков логического программирования приведен в книге Роиаг(а!увоз о/(.ояус Ргодгаттт8 [940]. Эффективные компиляторы Рго1о8 главным образом основаны на модели абстрактной машины Уоррена (%аггеп АЬзггасг Мас[йпе — %АМ), разработанной Дэвидом Г.Д. Уорреном [1556]. Ван Рой ]1536) показал, что благодаря применению дополнительных методов организации работы компилятора, таких как логический вывод типов, программы Рго!ой становятся способными конкурировать по быстродействию с программами С.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
