Взаимосвязь между языком Prolog и логикой

Язык 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), при которой определяется, входит ли конкретная перемен­ная в указанный терм. Если бы такая проверка вхождения применялась при согла­совании, эта операция стала бы неэффективной.