БИБЛИОГРАФИЧЕСКИЕ И ИСТОРИЧЕСКИЕ ЗАМЕТКИ
Логический вывод широко исследовался древнегреческими математиками. Аристотель тщательно исследовал один из типов логического вывода, называемый силлогизмом, который представляет собой своего рода правило логического вывода. Силлогизмы Аристотеля включали элементы логики первого порядка, такие как кванторы, но были ограничены унарными предикатами. Силлогизмы классифицировались по "фигурам" и "модусам", в зависимости от порядка термов (которые следовало бы назвать предикатами) в высказываниях и от степени общности (которую теперь принято интерпретировать с помощью кванторов), применяемой к каждому терму, а также с учетом того, является ли каждый терм отрицаемым. Наиболее фундаментальным силлогизмом является тот, который относится к первой фигуре первого модуса:
Все S суть М. Все М суть Р.
Следовательно, все S суть Р.
Аристотель пытался доказать истинность других силлогизмов, "приводя" их к силлогизмам первой фигуры. Описание того, в чем должно состоять такое "приведение", оказалось гораздо менее точным по сравнению с описанием, в котором были охарактеризованы сами фигуры и модусы силлогизмов.
Готтлоб Фреге, который разработал полную логику первого порядка в 1879 году, основал свою систему логического вывода на большой коллекции логически правильных схем и единственном правиле логического вывода — правиле отделения (Modus Ponens). Фреге воспользовался тем фактом, что результат применения любого правила логического вывода в форме "Из Р вывести ?>" можно моделировать путем применения к высказыванию Р правила отделения наряду с логически правильной схемой Р => Q. Такой "аксиоматический" стиль представления знаний, в котором наряду с правилом отделения использовался целый ряд логически правильных схем, был принят на вооружение после Фреге многими логиками; наиболее замечательным является то, что этот стиль использовался в основополагающей книге Principia Mathematica [1584].
В подходе на основе натуральной дедукции (natural deduction), который был введен Герхардом Генценом [541] и Станиславом Яськовским [725], основное внимание было сосредоточено не на аксиоматических системах, а на правилах логического вывода. Натуральная дедукция получила название "натуральной", поскольку в ней не требуется преобразование в нормальную форму (неудобную для восприятия человеком), а также в связи с тем, что в ней применяются такие правила логического вывода, которые кажутся естественными для людей. Правитц [1235] посвятил описанию натуральной дедукции целую книгу. Галье [515] применил подход Гентцена для разъяснения теоретических основ автоматизированной дедукции.
Крайне важным этапом в разработке глубокого математического анализа логики первого порядка явилось изобретение формы представления в виде импликационных выражений (clausal form). Уайтхед и Рассел [1584] описали так называемые правила прохождения (rules of passage) (фактически этот термин принадлежит Эрбрану [650]), которые используются для перемещения кванторов в переднюю часть формул. Торальфом Сколемом [1424] были достаточно своевременно предложены ско-лемовские константы и сколемовские функции. Общая процедура сколемизации, наряду с важным понятием универсума Эрбрана, описана в [1425].
Крайне важную роль в разработке автоматизированных методов формирования рассуждений, как до, так и после введения Робинсоном правила резолюции, играет теорема Эрбрана, названная в честь французского логика Жака Эрбрана [650]. Это отражается в применяемом нами термине "универсум Эрбрана", а не "универсум Сколема", даже несмотря на то, что это понятие в действительности было открыто Сколемом. Кроме того, Эрбран может считаться изобретателем операции унификации. Гёдель [565], опираясь на идеи Сколема и Эрбрана, сумел показать, что для логики первого порядка имеется полная процедура доказательства. Алан Тьюринг [1518] и Алонсо Черч [255] практически одновременно продемонстрировали, используя очень разные доказательства, что задача определения общезначимости в логике первого порядка не имеет решения. В превосходной книге Эндертона [438] все эти результаты описаны в строгой, но труднодоступной для понимания манере.
Хотя Маккарти [1009] предложил использовать логику первого порядка для представления знаний и формирования рассуждений в искусственном интеллекте, первые подобные системы были разработаны логиками, заинтересованными в получении средств автоматического доказательства математических теорем. Впервые применение метода пропозиционализации и теоремы Эрбрана предложено Абрахамом Робинсоном, а Гилмор [556] написал первую программу, основанную на этом подходе. Дэвис и Патнем [336] применили форму представления в виде импликационных выражений и разработали программу, в которой предпринимались попытки поиска противоречий путем подстановки элементов универсума Эрбрана вместо переменных для получения базовых выражений, а затем поиска пропозициональных противоречивостей среди этих базовых выражений. Правиц [1234] разработал ключевую идею, позволяющую использовать для управления процессом поиска тенденцию к обнаружению пропозициональных противоречивостей и вырабатывать термы из универсума Эрбрана, только если это необходимо для определения пропозициональной противоречивости. После дальнейшей разработки этой идеи другими исследователями Дж.Э. Робинсон (который не связан родством с Абрахамом Робинсоном) пришел к созданию метода резолюции [1298]. Примерно в то же время советским исследователем С. Масловым [994], [995] на основе немного иных принципов был разработан так называемый инверсный метод, который характеризуется некоторыми вычислительными преимуществами над пропозиционализацией. Метод соединения Вольфганга Бибеля [123] может рассматриваться как расширение этого подхода.
После разработки метода резолюции исследования в области логического вывода первого порядка стали развиваться в нескольких разных направлениях. В искусственном интеллекте метод резолюции применялся для создания систем поиска ответов на вопросы Корделлом Грином и Бертрамом Рафаэлем [593]. Несколько менее формальный подход был принят Карлом Хьюиттом [651]. Разработанный им язык Planner, хотя и не был полностью реализован, явился предшественником логического программирования и включал директивы для прямого и обратного логического вывода и для отрицания как недостижения цели. А подмножество этого языка, известное как Micro-Planner [1475], было реализовано и использовалось в системе понимания естественного языка Shrdlu [1601]. В ранних реализациях систем искусственного интеллекта большие усилия направлялись на разработку структур данных, которые должны были обеспечить эффективную выборку фактов; эти работы описаны в книгах по программированию для искусственного интеллекта [240], [479], [1148].
В начале 1970-х годов в искусственном интеллекте полностью утвердился метод прямого логического вывода как легко доступная пониманию альтернатива методу резолюции. Прямой логический вывод использовался в самых различных системах, начиная от программы автоматического доказательства геометрических теорем Не-винса [1123] и заканчивая экспертной системой R1 для разработки конфигурации компьютеров VAX [1026]. Приложения искусственного интеллекта обычно охватывают большое количество правил, поэтому было важно разработать эффективную технологию согласования с правилами, особенно для инкрементных обновлений. Для поддержки таких приложений была разработана технология продукционных систем. Язык продукционных систем Ops-5 [197], [482] использовался для экспертной системы R1 и для когнитивной архитектуры Soar [880]. В язык Ops-5 был включен процесс согласования с помощью rete-алгоритма [483]. Архитектура Soar, позволяющая вырабатывать новые правила для кэширования результатов предыдущих вычислений, способна создавать очень большие множества правил; например, в системе TacAir-Soar, предназначенной для управления тренажером, моделирующим самолет-истребитель [743], количество правил превышало один миллион. Язык
CLIPS [1626] продукционных систем на основе языка С, разработанный в NASA, обеспечивал лучшую интеграцию с другими программными, аппаратными и сенсорными системами и использовался для автоматизации космической станции и разработки нескольких военных приложений.
Большой вклад в понимание особенностей прямого логического вывода внесли также работы в области исследований, известной как дедуктивные базы данных. Исследования в этой области начались с симпозиума, организованного в Тулузе в 1977 году Джеком Минкером, который собрал вместе специалистов в области логического вывода и систем баз данных [514]. В опубликованном сравнительно недавно историческом обзоре [1264] сказано: "Дедуктивные системы [баз данных] были попыткой адаптировать язык Prolog, воплощающий видение мира с «малыми данными», к миру «больших данных»". Таким образом, цель разработок в этой области состоит в объединении технологии баз данных, которая предназначена для выборки больших множеств фактов, с технологией логического вывода на основе языка Prolog, в которой обычно осуществляется выборка одновременно только одного факта. К числу работ в области дедуктивных баз данных относятся [228] и [1525].
Важная работа, выполненная Чандрой и Нарелом [231], а также Ульманом [1524], привела к признанию языка Datalog в качестве стандартного языка для дедуктивных баз данных. Кроме того, стал стандартным "восходящий" логический вывод, или прямой логический вывод, отчасти потому, что данный метод позволяет избежать проблем, обусловленных незавершаемыми и избыточными вычислениями, которые возникают при обратном логическом выводе, и отчасти потому, что имеет более естественную реализацию в терминах основных операций реляционной базы данных. Разработка метода магических множеств для перезаписи правил Бансильоном и др. [67] позволила воспользоваться в прямом логическом выводе преимуществами целенаправленности, свойственными обратному логическому выводу. Методы табулированного логического программирования (с. 1), вступившие в конкурентную борьбу с другими методами, заимствовали преимущества динамического программирования от прямого логического вывода.
Большой вклад в понимание сложностей логического вывода внесло сообщество пользователей дедуктивных баз данных. Чандра и Мерлин [232] впервые показали, что задача согласования единственного нерекурсивного правила (в терминологии баз данных — конъюнктивного запроса) может оказаться NP-трудной. Купер и Варди [870] предложили использовать понятие сложности данных (т.е. сложности как функции размера базы данных, в которой размер правила рассматривается как постоянный) в качестве подходящего критерия эффективности получения ответов на запросы. Готтлоб и др. [586] обсудили связь между конъюнктивными запросами и задачами удовлетворения ограничений, показав, как можно использовать способ декомпозиции гипердерева для оптимизации процесса согласования.
Как уже упоминалось выше, процедуры обратного логического вывода, применяемые для логического вывода, впервые появились в разработанном Хьюиттом языке Planner [651 ]. Но логическое программирование как таковое развивалось независимо от этого направления разработок. Ограниченная форма линейной резолюции, называемая SL-резолюцией, была разработана Ковальским и Кюнером [853] на основе метода устранения моделей Лавленда [947]; после применения этого метода к определенным выражениям он принял вид метода SLD-резолюции, который предоставил возможность осуществлять интерпретацию определенных выражений как программ [849—851]. Между тем в 1972 году французский исследователь Ален Колмерор разработал и реализовал Prolog в целях синтаксического анализа текста на естественном языке; первоначально выражения Prolog предназначались для использования в качестве правил контекстно-свободной грамматики [285], [1311]. Основная часть теоретических основ логического программирования разработана Ковальским в сотрудничестве с Колмерором. Семантическое определение с использованием наименьших фиксированных точек предложено Ван Эмденом и Ковальским [1530]. Ковальский и Коэн [274], [852] подготовили хорошие исторические обзоры истоков языка Prolog. Теоретический анализ основ языка Prolog и других языков логического программирования приведен в книге Foundations of Logic Programming [940].
Эффективные компиляторы Prolog главным образом основаны на модели абстрактной машины Уоррена (Warren Abstract Machine — WAM), разработанной Дэвидом Г.Д. Уорреном [1556]. Ван Рой [1536] показал, что благодаря применению дополнительных методов организации работы компилятора, таких как логический вывод типов, программы Prolog становятся способными конкурировать по быстродействию с программами С. Рассчитанный на 10 лет исследовательский проект создания компьютера пятого поколения, который был развернут в Японии в 1982 году, опирался полностью на язык Prolog, применяемый в качестве средства разработки интеллектуальных систем.
Методы предотвращения нежелательного зацикливания в рекурсивных логических программах были разработаны независимо Смитом и др. [1434], а также Тамаки и Сато [1487]. Кроме того, последняя статья включала данные о методе запоминания, предназначенном для логических программ, который интенсивно разрабатывался в качестве метода табулированного логического программирования Дэвидом С. Уорреном. Свифт и Уоррен [1483] показали, как дополнить машину WAM для обеспечения табуляции, что позволяет добиться быстродействия программ Datalog, превышающего на порядок быстродействие дедуктивных систем баз данных с прямым логическим выводом.
Первые теоретические работы по логическому программированию в ограничениях были выполнены Джаффаром и Лассе [722]. Джаффар и др. [723] разработали систему CLP(R) для обработки ограничений с действительными значениями. В [724] приведено описание обобщенной машины WAM, на основе которой создана машина CLAM (Constraint Logic Abstract Machine — абстрактная машина логики ограничений) для разработки спецификаций различных реализаций систем CLP. В [10] описан сложный язык Life, в котором методы CLP сочетаются с функциональным программированием и формированием рассуждений в логике наследования. В [820] описан перспективный проект использования логического программирования в ограничениях в качестве основы архитектуры управления в реальном времени, которая может применяться для создания полностью автоматических средств вождения самолетов (автопилотов).
Объем литературы по логическому программированию и языку Prolog очень велик. Одной из первых книг по логическому программированию явилась книга Logic for Problem Solving [851]. Языку Prolog посвящены, в частности, книги [175], [270] и [1405]. Превосходный обзор тематики CLP приведен в [987]. До его закрытия в 2000 году официальным журналом для публикаций в этой области был Journal of Logic Programming] теперь вместо него выпускается журнал Theory and Practice of Logic Programming. К числу основных конференций по логическому программированию относятся International Conference on Logic Programming (ICLP) и International Logic Programming Symposium (ILPS).
Исследования в области автоматического доказательства математических теорем начались еще до того, как были впервые разработаны полные логические системы первого порядка. В разработанной Гербертом Гелернтером программе Geometry Theorem Prover [532] использовались методы эвристического поиска в сочетании с диаграммами для отсечения ложных подцелей; с помощью этой программы удалось обосновать некоторые весьма сложные результаты математических исследований в области евклидовой геометрии. Но с тех пор взаимодействие таких научных направлений, как автоматическое доказательство теорем и искусственный интеллект, не слишком велико.
На первых порах основные усилия ученых были сосредоточены на проблемах полноты. Вслед за появлением оригинальной статьи Робинсона в работах [1619] и [1620] были предложены правила демодуляции и парамодуляции для формирования рассуждений с учетом отношения равенства. Эти правила были также разработаны независимо в контексте систем перезаписи термов [811]. Внедрение средств формирования рассуждений с учетом отношения равенства в алгоритм унификации было осуществлено Гордоном Плоткиным [1217]; применение таких средств было также предусмотрено в языке Qlisp [1339]. В [752] приведен обзор средств унификации с учетом отношения равенства на основе процедур перезаписи термов. Эффективные алгоритмы для стандартной унификации были разработаны Мартелли и Монтанари [989], а также Патерсоном и Вегманом [1181].
Кроме средств формирования рассуждений с учетом отношения равенства, в программы автоматического доказательства теорем были включены всевозможные процедуры принятия решений специального назначения. В [1120] предложена получившая широкое распространение схема интеграции подобных процедур в общую схему формирования рассуждений; к другим методам относятся "резолюция теории" Стикеля [1462] и "специальные отношения" Манна и Валдингера [978].
Для метода резолюции был предложен целый ряд стратегий управления, начиная со стратегии предпочтения единичного выражения [1616]. В [1617] была предложена стратегия с использованием множества поддержки, которая позволяет обеспечить определенную целенаправленность резолюции. Линейная резолюция впервые была предложена в [948]. В [537, глава 5] приведен краткий, но исчерпывающий анализ всего разнообразия стратегий управления.
В [602] описана одна из первых программ автоматического доказательства теорем, Sam, которая позволила решить одну из открытых проблем в теории решеток. В [1621] приведен краткий обзор того, какой вклад был внесен с помощью программы автоматического доказательства теорем Aura в решение открытых проблем в различных областях математики и логики. Это описание продолжено в [1018], где перечислены достижения программы Otter, преемника программы Aura, в решении открытых проблем. В [1563] описана программа Spass— одна из сильнейших современных программ автоматического доказательства теорем. Основным справочником по программе автоматического доказательства теорем Бойера—Мура является книга A Computational Logic [165]. В [1463] рассматривается система РТТР (Prolog Technology Theorem Prover), в которой сочетаются преимущества компиляции Prolog с полнотой устранения моделей [947]. Еще одной широко применяемой программой автоматического доказательства теорем, основанной на этом подходе, является SETHEO [915]; она способна выполнять несколько миллионов логических выводов в секунду на рабочих станциях модели 2000. Эффективной программой автоматического доказательства теорем, реализованной всего лишь в 25 строках на языке Prolog, является LeanTaP [91].
Одни из первых работ в области автоматизированного синтеза программ были выполнены Саймоном [1416], Грином [591], а также Манна и Валдингером [976]. В трансформационной системе Бурстолла и Дарлингтона [211] используется формирование рассуждений с учетом отношения равенства для синтеза рекурсивных программ. Одной из самых сильных современных систем является Kids [1435], [1436]; она действует в качестве помощника эксперта. В [979] приведено учебное введение с описанием современного состояния дел в этой области, в котором основное внимание уделено описанию собственного дедуктивного подхода этих авторов. В книге Automating Software Design [954] собрано множество статей из этой области. Обзор примеров использования логики в проектировании аппаратных средств приведен в [791]; в [267] рассматривается применение метода проверки по модели для диагностирования аппаратных средств.
Хорошим справочником по темам полноты и неразрешимости является книга Computability and Logic [ 150]. Многие ранние статьи в области математической логики можно найти в книге From Frege to Godel: A Source Book in Mathematical Logic [1532]. Официальным журналом для публикаций в области чистой математической логики (в отличие от автоматизированного дедуктивного логического вывода) является The Journal of Symbolic Logic. К числу учебников, посвященных автоматизированному дедуктивному логическому выводу, относятся классическая книга Symbolic Logic and Mechanical Theorem Proving [233], а также более новые работы [124], [776] и [1618]. Антология Automation of Reasoning [1408] включает много важных ранних статей по автоматизированному дедуктивному логическому выводу. Другие исторические обзоры приведены в [206] и [949]. Основным журналом для публикаций в области автоматического доказательства теорем является Journal of Automated Reasoning, а главной конференцией — ежегодно проводимая конференция Conference on Automated Deduction (CADE). Кроме того, исследования в области автоматического доказательства теорем тесно связаны с работами по использованию логики при анализе программ и языков программирования, которым посвящена основная конференция Logic in Computer Science.