Рассел С., Норвиг П. Искусственный интеллект. Современный подход (2-е изд., 2006) (1245267), страница 116
Текст из файла (страница 116)
Рассчитанный на 10 лет исследовательский проект создания компьютера пятого поколения, который бып развернут в Японии в !982 году, опирался полностью на язык Рго!о8, применяемый в качестве средства разработки интеллектуальных систем. Методы предотвращения нежелательного зацикливания в рекурсивных логических программах были разработаны независимо Смитом и др.
[1434), а также Тамаки и Сато [!487]. Кроме того, последняя статья включала данные о методе запоминания, предназначенном для логических программ, который интенсивно разрабатывался в качестве метода табулированного логического программирования Дэвидом С. Уорреном. Свифт и Уоррен [1483] показали, как дополнить машину %АМ для обеспечения табуляции, что позволяет добиться быстродействия программ Оа!а!о8, превышающего на порядок быстродействие дедуктивных систем баз данных с прямым логическим выводом. Первые теоретические работы по логическому программированию в ограничениях были выполнены Джаффаром и Лассе [722].
Джаффар и др. [723) разработали систему С].Р(В) для обработки ограничений с действительными значениями. В [724) приведено описание обобшенной машины %АМ, на основе которой создана машина С(.АМ (Сова!та)пг ].о8!с АЬзггас! Мас[йпе — абстрактная машина логики ограничений) для разработки спецификаций различных реализаций систем С!.Р. В [10] описан сложный язык Ые, в котором методы С!.Р сочетаются с функциональным программированием и формированием рассуждений в логике наследования. В [820) описан перспективный проект использования логического программирования в ограничениях в качестве основы архитектуры управления в реальном времени, которая может применяться для создания полностью автоматических средств вождения самолетов (автопилотов).
Обьем литературы по логическому программированию и языку Рго1о8 очень велик. Одной из первых книг по логическому программированию явилась книга Ео8(с /ог РгоЫет 5оlил8 [851]. Языку Рго!о8 посвящены, в частности, книги [!75], [270] и [! 405]. Превосходный обзор тематики С!.Р приведен в [987).
До его закрытия в 2000 году официальным журналом для публикаций в этой области был зоигпа! о7 Еох(с РгодгаттГлд; теперь вместо него выпускается журнал 7аеогу алН Ргаспсе о( Ео8(с Рго8гатт)и8. К числу основных конференций по логическому программированию 434 Часть П1. Знания и рассуждения относятся !пгегпабопа! Соп(егепсе оп 7о8(с Ргохгаттт8 (!СЕР) и 7пгегпаг(опа! 2о8(с Рго8гаттт8 Яутрогпит (! 1.РЯ). Исследования в области автоматического доказательства математических теорем начались еще ло того, как были впервые разработаны полные логические системы первого порядка.
В разработанной Гербертом Гелернтером программе Оеогпеггу Т)зеогеш Ргоуег [532] использовались методы эвристического поиска в сочетании с диаграммами для отсечения ложных подцелей; с помошью этой программы удалось обосновать некоторые весьма сложные результаты математических исследований в области евклидовой геометрии. Но с тех пор взаимодействие таких научных направлений, как автоматическое доказательство теорем и искусственный интеллект, не слишком велико. На первых порах основные усилия ученых были сосредоточены на проблемах полноты. Вслед за появлением оригинальной статьи Робинсона в работах [1619] и [1620] были предложены правила демодуляции и парамодуляции для формирования рассуждений с учетом отношения равенства.
Эти правила были также разработаны независимо в контексте систем перезаписи термов [8 ! 1]. Внедрение средств формирования рассуждений с учетом отношения равенства в алгоритм унификации было осушествлено Гордоном Плоткиным [1217]; применение таких средств было также предусмотрено в языке О1гвр [1339]. В [752] приведен обзор средств унификации с учетом отношения равенства на основе процедур перезаписи термов. Эффективные алгоритмы для стандартной унификации были разработаны Мартелли и Монтанари [989], а также Патерсоном и Вегманом [1181].
Кроме срелств формирования рассуждений с учетом отношения равенства, в программы автоматического доказательства теорем были включены всевозможные процедуры принятия решений специального назначения. В [1! 20] предложена получившая широкое распространение схема интеграции подобных процедур в общую схему формирования рассуждении; к другим методам относятся "резолюция теории" Стикеля [1462] и "специальные отношения" Манна и Валдингера ]978]. Для метода резолюции был предложен целый ряд стратегий управления, начиная со стратегии предпочтения единичного выражения ]1616]. В [1617] была предложена стратегия с использованием множества поддержки, которая позволяет обеспечить определенную целенаправленность резолюции. Линейная резолюция впервые была предложена в [948]. В [537, глава 5) приведен краткий, но исчерпываюший анюгиз всего разнообразия стратегий управления.
В [602] описана одна из первых программ автоматического доказательства теорем, Яаш, которая позволила решить одну из открытых проблем в теории решеток. В [1621] приведен краткий обзор того, какой вклад был внесен с помошью программы автоматического доказательства теорем Ацга в решение открытых проблем в различных областях математики и логики. Это описание продолжено в ]10 !8], где перечислены достижения программы Оссег, преемника программы Ацга, в решении открытых проблем.
В [1563] описана программа Ярая — одна из сильнейших современных программ автоматического доказательства теорем. Основным справочником по программе автоматического доказательства теорем Бойера — Мура является книга А Сотригагита) 7.о81с [165]. В [! 463] рассматривается система РТТР (Рго1о8 Тесйпо!ойу Тйеогегп Ргоуег), в которой сочетаются преимущества компиляции Рго!о8 с полнотой устранения моделей [947]. Еще одной широко применяемой программой автоматического доказательства теорем, основанной на этом подходе, является ЯЕТНЕО [915]; она способна выполнять несколько миллионов логических выводов Глава 9.
Логический вывод в логике первого порядка 435 в секунду на рабочих станциях модели 2000. Эффективной программой автоматического доказательства теорем, реализованной всего лишь в 25 строках на языке Рго!ой, является ЕеапТаР [91[. Одни из первых работ в области автоматизированного синтеза программ были выполнены Саймоном [1416[, Грином [591[, а также Манна и Валдингером [976[. В трансформационной системе Бурстолла и Дарлингтона [211[ используется формирование рассуждений с учетом отношения равенства для синтеза рекурсивных программ. Одной из самых сильных современных систем является КЫз [14351, [1436); она действует в качестве помошника эксперта.
В [979) приведено учебное введение с описанием современного состояния дел в этой области, в котором основное внимание уделено описанию собственного дедуктивного подхода этих авторов. В книге Аи(ота((пя ВоФигаге Резфп [954[ собрано множество статей из этой области. Обзор примеров использования логики в проектировании аппаратных средств приведен в [791[; в [267[ рассматривается применение метода проверки по модели лля диагностирования аппаратных средств. Хорошим справочником по темам полноты и неразрешимости является книга Сотри(а(п(((у ат( 1оя(с [150[.
Многие ранние статьи в области математической логики можно найти в книге В от рге8е (о боде(: А Воигсе Воо(г (п Ма(пети((са( 7.о8(с [1532[. Официальным журналом для публикаций в области чистой математической логики (в отличие от автоматизированного дедуктивного логического вывода) является Тйе Уоигпа( оТ5гтбо((с 7.оя(с. К числу учебников, посвященных автоматизированному дедуктивному логическому выводу, относятся классическая книга ВутЬо((с боя(с апг( Месйап(са( Тйеогет Ргоип8 [233[, а также более новые работы [124), [776[ и [1618[.
Антология Аи(отацоп оТ((еазопслх [!408[ включает много важных ранних статей по автоматизированному дедуктивному логическому выводу. Другие исторические обзоры приведены в [206! и [949[. Основным журналом для публикаций в области автоматического доказательства теорем является уоигпа( оТАи(ота(ег( Веазоптй, а главной конференцией — ежегодно проводимая конференция Сгп(регепсе оп Аи(ота(ег( (3ег(ис((оп (САРЕ). Кроме того, исследования в области автоматического доказательства теорем тесно связаны с работами по использованию логики при анализе программ и языков программирования, которым посвящена основная конференция 1оя(с и Сотри гег Бс(епсе.
УПРАЖНЕНИЯ 9.1. Докажите на основании главных логических принципов, что процедура конкретизации с помощью квантора всеобщности является непротиворечивой и что процедура конкретизации с помощью квантора существования позволяет получить базу знаний, эквивалентную с точки зрения логического вывода. Представляется вполне обоснованным утверждение, что из отдельного факта Ьй(сея(гезху, гсеСтеат) можно вывести высказывание Зх Ъд(сев (х, тсеСгеат) . Запишите общее правило логического вывода, правило ак введения квантора существования, позволяющее узаконить такой логический вывод. Тщательно сформулируйте условия, которым должны удовлетворять переменные и термы, участвующие в этом выводе. 436 Часть )П.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
