БИБЛИОГРАФИЧЕСКИЕ И ИСТОРИЧЕСКИЕ ЗАМЕТКИ
Даже в логике Аристотеля предпринимались попытки применять обобщения к объектам, но датой рождения подлинной логики первого порядка стало появление книги Готтлоба Фреге Begriffschrift ("Система обозначения понятий") [496], в которой были впервые введены кванторы. Предложенная в этой книге возможность вкладывать кванторы была большим шагом вперед, но Фреге использовал громоздкую систему обозначений. (Один из примеров таких обозначений приведен на первой странице обложки данной книги.) Современная система обозначений для логики первого порядка появилась в основном благодаря Джузеппе Пеано [1185], но ее семантика практически идентична семантике, предложенной в работе Фреге. Хотя сейчас это кажется довольно странным, но аксиомы Пеано в значительной степени обязаны своим появлением работам Грассмана [588] и Дедекинда [375].
Основным барьером на пути разработки логики первого порядка была полная концентрация усилий ученых на одноместных предикатах за счет исключения из рассмотрения многоместных реляционных предикатов. Такое сосредоточение на одноместных предикатах в логических системах было почти повсеместным, начиная от Аристотеля и включая Буля. Первая систематическая трактовка отношений была выполнена Аугустусом де Морганом [351], который цитировал следующий пример, чтобы показать, какого рода логические выводы не позволяет выполнять логика Аристотеля: "Все лошади — животные; поэтому голова лошади — это голова животного". Такой логический вывод неосуществим в логике Аристотеля, поскольку в любом допустимом правиле, способном поддерживать этот логический вывод, вначале необходимо проанализировать данное высказывание с использованием двухместного предиката "х— голова у". Логика отношений была глубоко исследована Чарльзом Сандерсом Пирсом [1196], который также разработал логику первого порядка независимо от Фреге, хотя и немного позднее [1197].
Леопольд Лёвенхейм дал систематическую трактовку теории моделей для логики первого порядка в 1915 году [951]. В его статье рассматривался также символ равенства как неотъемлемая часть логики. Результаты Лёвенхейма были дополнительно расширены Торальфом Сколемом [1424]. Альфред Тарский [1490], [1491] дал явное определение понятий истинности и модельно-теоретического выполнения в логике первого порядка с использованием теории множеств.
Первым, кто предложил использовать логику первого порядка в качестве инструментального средства для создания систем искусственного интеллекта, был Маккарти [1009]. Перспективы искусственного интеллекта на основе логики значительно расширились в результате разработки Робинсоном [1298] резолюции — описанной в главе 9 полной процедуры вывода для логики первого порядка. Подход, получивший название логицистского, зародился в Станфордском университете. Корделл Грин [591], [592] разработал первую систему формирования рассуждений в логике первого порядка, QA3, что привело к первым попыткам создания логического робота в институте SRI [466]. Логика первого порядка была применена Зохаром Манна и Ричардом Валдингером [976] для формирования рассуждений о программах, а позднее — Майклом Генезеретом [536] для формирования рассуждений об электронных схемах. В Европе для использования в лингвистическом анализе [285] и для создания общих декларативных систем [849] было разработано логическое программирование (ограниченная форма проведения рассуждений в логике первого порядка). Кроме того, в ходе разработки проекта LCF (Logic for Computable Functions) в Эдинбурге [580] был внесен большой вклад в вычислительную логику. История этих разработок будет описана более подробно в главах 9 и 10.
Существует целый ряд хороших современных вводных учебников по логике первого порядка. Одним из наиболее удобных для чтения является [1254]. В [438] эта область знаний рассматривается в перспективе, в большей степени ориентированной на математику. В высшей степени формальная трактовка логики первого порядка, наряду с описанием более сложных тем логики, предоставлена в [94]. В [977] приведено удобное для чтения введение в логику с точки зрения компьютерных наук. В [515] дано чрезвычайно строгое математическое описание логики первого порядка, наряду со значительным объемом материала, который может использоваться в области автоматического формирования рассуждений. В книге Logical Foundations of Artificial Intelligence [537] приведено не только солидное введение в логику, но и первое систематическое описание логических агентов с восприятиями и действиями.