Язык Prolog имеет непосредственное отношение к математической логике, поэтому его синтаксис и значение программ можно определить более кратко с использованием логических обозначений. И действительно, синтаксис языка Prolog часто определяют именно таким образом. Но подобное введение в Prolog предполагает, что читатель знаком с некоторыми понятиями математической логики. С другой стороны, безусловно, что знакомство с этими понятиями не требуется для изучения и использования языка Prolog как инструментального средства программирования, а в этом и состоит назначение данной книги. Для тех читателей, кто особенно заинтересован в изучении взаимосвязи между языком Prolog и логикой, ниже приведены некоторые основные указания, касающиеся определения этого языка в терминах математической логики, наряду с некоторыми подходящими источниками информации.
Синтаксис Prolog - это синтаксис предложений (формул) логики предикатов первого порядка, записанных в так называемой форме предложении (в конъюнктивной нормальной форме, в которой кванторы не записываются явно) и дополнительно ограниченных хорновскими предложениями (формулами логики предикатов первого порядка, которые имеют самое большее один положительный литерал, называемыми также хорновскими дизъюнктами). В [32] опубликована программа Prolog, которая преобразует формулы исчисления предикатов первого порядку в форму предложений. Процедурное значение программы Prolog основано на принципе резолюции, применимом для автоматического доказательства теорем, который был представлен Робинсоном в его классической статье [131]. В языке Prolog для доказательства теоремы резолюции используется специальная стратегия, называемая SLD. Введение в проблематику исчисления предикатов первого порядка и доказательства теорем на основе резолюций можно найти в нескольких книгах, посвященных общим вопросам искусственного интеллекта ([58]; [60]; [126]; [133]; см. также [51]). Математические проблемы, касающиеся свойств процедурного значения Prolog по отношению к логике, проанализированы в [89].
Операция согласования в языке Prolog соответствует тому действию, которое в логике называют унификацией. Но мы избегаем использования термина "унификация", поскольку в большинстве систем Prolog по требованиям повышения эффективности согласование реализовано таким способом, что оно не совсем точно соответствует унификации (см. упр. 2.10). Но с практической точки зрения согласование вполне можно рассматривать как операцию, аналогичную унификации. Тем не менее для правильной унификации требуется проведение так называемой проверни вхождения (occurs check), при которой определяется, входит ли конкретная переменная в указанный терм. Если бы такая проверка вхождения применялась при согласовании, эта операция стала бы неэффективной.
