Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

goal <описание цели> clauses <факты и правила> /* Комментарии */ Большинство программ содержат только часть из указанных разделов. Ме­ ханизм ПРОЛОГа состоит в том, чтобы доказать истинность цели и (или) найти значение переменного цели, при котором цель истинна. Вычисления всегда на­ чинаются с цели и рассматриваются возможные варианты нахождения резоль­ вент. Целью данного пособия не является изложение языка ПРОЛОГ. Эти пара­ графы только иллюстрируют, как работает логика в многообещающем языке ПРОЛОГ. § 13. ПРОЛОГ и логика предикатов Следуя работе [23] отметим следующие взаимосвязи между языком ПРОЛОГ и логикой предикатов. В логическом программировании, как уже указано выше, мы имеем дело с особым классом формул логики предикатов, а именно, с хорновскими дизъ­ юнктами, которые в свою очередь, являются замкнутыми формулами. Следова­ тельно, в логическом программировании имеем дело с подмножеством формул логики предикатов. Язык ПРОЛОГ является стратегией вывода заключений из начальных допущений (фактов и правил) и можно выделить следующие воз­ можные варианты: (1) чистый ПРОЛОГ; (2) реальный ПРОЛОГ. Чистый ПРОЛОГ не содержит никаких средств управления вычислением, так называемых нелогических операторов. Реальный ПРОЛОГ является расши­ рением чистого ПРОЛОГа за счет наличия нелогических операторов, за счет добавления отсечений. При этом теоремы полноты логики предикатов, спра­ ведливые для чистого ПРОЛОГ а, перестают быть таковыми в реальном ПРОЛОГ е. в чистом ПРОЛОГе теорема Робинсона (теорема 3.9) гарантируют, что ал­ горитм унификации всегда завершится, и при этом либо будут обнаружены все значения переменных, при которых осуществляется унификация, либо будет указано, что это невозможно осуществить. Вводя, нелогические операторы, мы коренным образом изменяем эти воз­ можности. Отсекая поддеревья в дереве вычислений, мы можем исключить возможность программе найти те значения переменных, при которых возможна унификация. Поэтому, хотя нелогические операторы придают программирова­ нию в реальном ПРОЛОГе большую гибкость, но в этом случае не имеем га­ рантии того, что программы будут вычислять правильные результаты. 90