Главная arrow книги arrow Копия Глава 9. Логический вывод в логике первого п arrow Библиографические и исторические заметки
Библиографические и исторические заметки

Методы предотвращения нежелательного зацикливания в рекурсивных логических программах были разработаны независимо Смитом и др. [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] использовались методы эвристического поиска в сочетании с диаграммами для отсечения ложных подцелей; с помощью этой программы удалось обосновать некоторые весьма сложные результаты математических исследований в области евклидовой геометрии. Но с тех пор взаимодействие таких научных направлений, как автоматическое доказательство теорем и искусственный интеллект, не слишком велико.